Function bad_proj_prop5

crates/kernel/src/tutorial/defeq.rs:1966–1982

()

    let mut env = prop_structure_env();
    let id = mk_prop_structure_proj_test(
      &mut env,
      "projProp2",
      cnst("PUnit", &[usucc(uzero())]),
      1,
    );
    check_rejects(&mut env, &id);
  }

  /// projProp3 (good): idx=2, aSecondProof : PUnit.{0} — proof before dependent data
  #[test]
  fn good_proj_prop3() {
    let mut env = prop_structure_env();
    let id = mk_prop_structure_proj_test(
      &mut env,
      "projProp3",
      cnst("PUnit", &[uzero()]),
      2,
    );
    check_accepts(&mut env, &id);
  }