proposition: Lemma clos_rt_clos_t {X R x y }: clos_trans _ R x y -> clos_refl_trans X R x y.
proof: Proof. elim; eauto using clos_refl_trans with nocore. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun