* Initial invocation: - Patience on me to gain peace and perfection! -
*)
-include "ground_2/lib/star.ma".
+include "ground_2/lib/relations.ma".
include "basic_2/notation/constructors/item0_0.ma".
include "basic_2/notation/constructors/snitem2_2.ma".
]
qed-.
-lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥.
+(* Basic_2A1: was: discr_tpair_xy_y *)
+lemma discr_apair_xy_y: ∀B,A. ②B. A = A → ⊥.
#B #A elim A -A
[ #H destruct
| #Y #X #_ #IHX #H elim (destruct_apair_apair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)