proposition: Lemma ordinal_induction : forall (p:EP), (forall z:E,(forall u:E, inc u z -> p u)-> p (union z)) -> (forall u :E, p u -> p (tack_on u u)) -> (forall o:E, is_ordinal o -> p o).
proof: Proof. ir. util (lgs_induction (f:=ID) (p:= p)). am. am. ap H2. am. Qed.
imports: Arith transfinite