proposition: Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z), (eq_trans p q = eq_trans p r) -> q = r.
proof: Proof. intros. destruct p. simpl in H. destruct r. simpl in H. rewrite eq_trans_refl_l in H. exact H. Qed.
imports: Coq.Logic.FunctionalExtensionality