proposition: Lemma power_clos_trans (T : X -> X -> Prop) k : inclusion _ (power k T) (clos_trans _ T).
proof: Proof. intros x y. induction k in x, y |- *. simpl. now constructor. simpl. intros [z [Pxz Tzy]]. econstructor 2. apply IHk; eauto. constructor. auto. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)