proposition: Lemma ctr_from_ct X (T : X -> X -> Prop): forall x y, clos_trans_1n X T x y -> clos_refl_trans X T x y.
proof: Proof. intros x y CT. induction CT. constructor 1. apply H. econstructor 3. constructor 1. apply H. apply IHCT. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)