---

Step * 1 1 of Lemma sub-corec-family


1. P : Type
2. H : (P ⟶ Type) ⟶ P ⟶ Type
3. ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
4. ⋂n:ℕ. H (H^n (λp.Top)) ⊆ H ⋂n:ℕ. H^n (λp.Top)
5. p : P@i
6. n : ℕ
⊢ (⋂n:ℕ. (H^n (λp.Top) p)) ⊆r (H (H^n (λp.Top)) p)
BY
{ TACTIC:(Subst' H (H^n (λp.Top)) ~ H^n + 1 (λp.Top) 0 THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:

1.  P  :  Type
2.  H  :  (P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
3.  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].  \mcap{}n:\mBbbN{}.  H  (X  n)  \msubseteq{}  H  \mcap{}n:\mBbbN{}.  X  n
4.  \mcap{}n:\mBbbN{}.  H  (H\^{}n  (\mlambda{}p.Top))  \msubseteq{}  H  \mcap{}n:\mBbbN{}.  H\^{}n  (\mlambda{}p.Top)
5.  p  :  P@i
6.  n  :  \mBbbN{}
\mvdash{}  (\mcap{}n:\mBbbN{}.  (H\^{}n  (\mlambda{}p.Top)  p))  \msubseteq{}r  (H  (H\^{}n  (\mlambda{}p.Top))  p)


By

---

Latex:
TACTIC:(Subst'  H  (H\^{}n  (\mlambda{}p.Top))  \msim{}  H\^{}n  +  1  (\mlambda{}p.Top)  0  THEN  Try  (Complete  (Auto)))

---

Home Index