sorry, "i ≤ j” should be “i < j” actually:
∀i j. i < j ⇒ f (SUC i) ⊆ f j
------------------------------------
0. ∀n. f n ⊆ f (SUC n)
1. ∀n. 0 < n ⇒ f 0 ⊆ f n> Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > 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
