proposition: Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z.
proof: Proof. induction 1. - auto. - intros; right with y; eauto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation