Hi, I have the following goal to prove: (f : num -> ‘a set)
∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
------------------------------------
0. ∀n. f n ⊆ f (SUC n)
but how can I do the induction on … e.g. `j - i`?
—Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
