proposition: Lemma INJF_INJ {A : Type'} : forall f1 : nat -> nat -> A -> Prop, forall f2 : nat -> nat -> A -> Prop, ((@INJF A f1) = (@INJF A f2)) = (f1 = f2).
proof: Proof. intros f1 f2. apply prop_ext. 2: intro e; subst; reflexivity. intro e. apply fun_ext; intro x. apply fun_ext; intro y. apply fun_ext; intro a. generalize (ext_fun e (NUMPAIR x y)); clear e; intro e. generalize (ext_fun e a); clear e. unfold INJF. rewrite NUMFST_NUMPAIR, NUMSND_NUMPAIR. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance