proposition: Lemma clos_rt_t' {X : Type} (R : X -> X -> Prop) x y z : clos_trans _ R x y -> clos_refl_trans _ R y z -> clos_trans _ R x z.
proof: Proof. move=> H /clos_rt_rtn1_iff H'. elim: H' H; by eauto using clos_trans. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect