proposition: Lemma lgs_induction : forall (f:E1)(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 (f u))) -> (forall y:E, is_leq_gen_scale f y -> p y).
proof: Proof. ir. ap excluded_middle; uhg; ir. util (lgs_smallest_with_property (f:=f) (p:=(fun t:E=>~p t))). sh y. xd. nin H3; ee. cp (lgs_limit_or_tack H3). nin H6; nin H6; ee. ap H4. rw H7; ap H. ir. cp (H6 _ H8); ee. ap excluded_middle; uhg; ir. util (H5 u). am. am. uh H10; ee. ap H10. apply extensionality; am. ap H4. rw H8; ap H0. ap excluded_middle; uhg; ir. util (H5 x0). am. am. ap H7. ap H10. rw H8; rw tack_on_inc. ap or_intror; tv. Qed.
imports: Arith order