proposition: Lemma ordinal_inc_induction : forall (p:EP)(o:E), (forall u:E, (forall x:E, inc x u -> p x)-> p u) -> is_ordinal o -> p o.
proof: Proof. ir. util (chenille_induction (f:=ID) (p:=p)). ir. ap H. ir. ap H2. rw ordinal_chenille. am. ap leq_gen_ordinal. am. ap H1. ap ordinal_leq_gen_refl; am. Qed.
imports: Arith transfinite