proposition: Lemma clos_rst_rstn1 : forall x y, clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y.
proof: Proof. induction 1. - constructor 2 with x; auto with Relations. constructor 1. - constructor 1. - apply clos_rstn1_sym; auto. - eapply clos_rstn1_trans; eauto. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Relation