proposition: Lemma clos_refl_trans_ind_left : forall (x:A) (P:A -> Prop), 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 x P H H0 z H1. revert H H0. induction H1 as [x| |x y z H1 IH1 H2 IH2]; intros HP HIS; auto with sets. - apply HIS with x; auto with sets. - apply IH2. + apply IH1; auto with sets. + intro y0; intros; apply HIS with y0; auto with sets. apply rt_trans with y; auto with sets. Qed.
imports: Relation_Definitions Relation_Operators