proposition: Lemma id_trans_sym {A} (x y z : A) (p : x = y) (q : y = z) (r : x = z) : id_trans p q = r -> q = id_trans (id_sym p) r.
proof: Proof. destruct p, q. destruct 1. exact 1. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes