proposition: Lemma INJA_INJ {A : Type'} : forall a1 : A, forall a2 : A, ((@INJA A a1) = (@INJA A a2)) = (a1 = a2).
proof: Proof. intros a1 a2. apply prop_ext. 2: intro e; subst; reflexivity. intro e. generalize (ext_fun e 0); clear e; intro e. generalize (ext_fun e a2); clear e. unfold INJA. rewrite refl_is_True, is_True. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance