proposition: Lemma t_trans' {A : Type} {R : relation A} {x x' y z : A} : x = x' -> clos_trans R x y -> clos_trans R y z -> clos_trans R x' z.
proof: Proof. move=> ->. by apply: t_trans. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)