proposition: Lemma Equal_NT_equiv : Equivalence Equal_NT.
proof: Proof. apply Build_Equivalence; unfold Equal_NT in |- *. unfold Reflexive in |- *; intros T a; apply Refl. apply Build_Partial_equivalence. unfold Transitive in |- *; intros T1 T2 T3 H H0 a. apply Trans with (ApNT T2 a); auto. unfold Symmetric in |- *; intros T1 T2 H a. apply Sym; apply H. Qed.
imports: Functor Setoid_dup2