---

Step * of Lemma face-forall-map

No Annotations
∀[G,H:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[s:H.𝕀 j⟶ G].  (s ∈ H, (∀ (phi)s).𝕀 j⟶ G, phi)
BY
{ ((RepeatFor 2 (Intro) THEN (Assert H.𝕀 j⊢ BY Auto) THEN Intros)
   THEN (InstLemma `face-forall-type-subtype` [⌜H⌝;⌜(phi)s⌝]⋅ THENA Auto)
   THEN (InstLemma `context-subset-map` [⌜G⌝;⌜phi⌝;⌜H.𝕀⌝;⌜s⌝]⋅ THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN RepeatFor 2 (Thin (-1))
   THEN (Assert H.𝕀, (phi)s j⊢ BY
               Auto)
   THEN (Assert H, (∀ (phi)s).𝕀 j⊢ BY
               Auto)
   THEN BLemma `cube_set_map_subtype2` 
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,H:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[s:H.\mBbbI{}  j{}\mrightarrow{}  G].    (s  \mmember{}  H,  (\mforall{}  (phi)s).\mBbbI{}  j{}\mrightarrow{}  G,  phi)


By

---

Latex:
((RepeatFor  2  (Intro)  THEN  (Assert  H.\mBbbI{}  j\mvdash{}  BY  Auto)  THEN  Intros)
  THEN  (InstLemma  `face-forall-type-subtype`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}(phi)s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `context-subset-map`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  (Assert  H.\mBbbI{},  (phi)s  j\mvdash{}  BY
                          Auto)
  THEN  (Assert  H,  (\mforall{}  (phi)s).\mBbbI{}  j\mvdash{}  BY
                          Auto)
  THEN  BLemma  `cube\_set\_map\_subtype2` 
  THEN  Auto)

---

Home Index