proposition: Lemma clos_rst_rst1n_iff : forall x y, clos_refl_sym_trans R x y <-> clos_refl_sym_trans_1n R x y.
proof: Proof. split. - apply clos_rst_rst1n. - apply clos_rst1n_rst. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation