---

Step * of Lemma type-monotone-fun_exp

∀[F:Type ⟶ Type]. ∀[n,m:ℕ].  (F^n Void) ⊆r (F^m Void) supposing n ≤ m supposing Monotone(T.F[T])
BY
{ (Auto
   THEN Subst' m ~ n + (m - n) 0
   THEN Auto
   THEN (GenConcl ⌜(m - n) = k ∈ ℕ⌝⋅ THENA Auto')
   THEN Repeat ((RWO "fun_exp_add_apply<" 0 THENA Auto))
   THEN GenConclAtAddr [2;2]
   THEN ThinVar `m'
   THEN ThinVar `k') }

1
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. n : ℕ
4. v : Type
⊢ (F^n Void) ⊆r (F^n v)

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}[n,m:\mBbbN{}].    (F\^{}n  Void)  \msubseteq{}r  (F\^{}m  Void)  supposing  n  \mleq{}  m  supposing  Monotone(T.F[T])


By

---

Latex:
(Auto
  THEN  Subst'  m  \msim{}  n  +  (m  -  n)  0
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  Repeat  ((RWO  "fun\_exp\_add\_apply<"  0  THENA  Auto))
  THEN  GenConclAtAddr  [2;2]
  THEN  ThinVar  `m'
  THEN  ThinVar  `k')

---

Home Index