proposition: Lemma nprod_eq {A B} (z1 z2 : A × B) : nfst z1 = nfst z2 -> nsnd z1 = nsnd z2 -> z1 = z2.
proof: Proof. change z1 with ⟨nfst z1, nsnd z1⟩ ; change z2 with ⟨nfst z2, nsnd z2⟩. simpl ; intros -> -> ; reflexivity. Defined.
imports: Coq.Logic(EqdepFacts)