proposition: Lemma clos_rst1n_rst : forall x y, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y.
proof: Proof. induction 1. - constructor 2. - constructor 4 with y; auto. case s; [constructor 1 | constructor 3; constructor 1]; auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation