proposition: Lemma clos_trans_n1_left {R : X -> X -> Prop} x y z : R x y -> clos_trans_n1 _ R y z -> clos_trans_n1 _ R x z.
proof: Proof. induction 2. econstructor 2; eauto. constructor; auto. econstructor 2. eauto. auto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)