proposition: Lemma INJN_INJ {A : Type'} : forall n1 : nat, forall n2 : nat, ((@INJN A n1) = (@INJN A n2)) = (n1 = n2).
proof: Proof. intros n1 n2. apply prop_ext. 2: intro e; subst; reflexivity. intro e. generalize (ext_fun e n1); clear e; intro e. generalize (ext_fun e (el A)); clear e. unfold INJN. rewrite refl_is_True, sym, is_True. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance