proposition: Lemma inv_pp {A x y z} (p : x = y :> A) (q : y = z :> A) : eq_sym (eq_trans p q) = eq_trans (eq_sym q) (eq_sym p).
proof: Proof. case q; case p; reflexivity. Defined.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common