proposition: Lemma clos_refl_trans_ind_left : forall (x:A) (P:A -> Type), P x -> (forall y z:A, clos_refl_trans R x y -> P y -> R y z -> P z) -> forall z:A, clos_refl_trans R x z -> P z.
proof: Proof. intros. revert X X0. induction X1; intros; auto with Relations. { apply X0 with x; auto with Relations. } apply IHX1_2. { apply IHX1_1; auto with Relations. } intros. apply X0 with y0; auto with Relations. apply rt_trans with y; auto with Relations. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Relation