proposition: Lemma chenille_induction : forall f (p:EP), (forall x, leq_gen f x x -> (forall y, inc y (chenille f x) -> p y) -> p x) -> (forall z, leq_gen f z z -> p z).
proof: Proof. ir. apply leq_gen_induction with (f:= f) (p:= p). ir. ap H. am. ir. ap H2. rwi chenille_inc H3. xd. am. rwi chenille_inc H3; xd. am. Qed.
imports: Arith order