proposition: Lemma noc_hetero_inv {A} (e e' : &{ p : &{ x : A & A } & eq p.1 p.2 }) (H : NoC_hetero e e') : e = e'.
proof: Proof. destruct e as [[x y] e]. destruct e' as [[x' y'] e'']. simpl in *. destruct e, e''. red in H. destruct H. reflexivity. Defined.
imports: Equations(Equations)