---

Step * of Lemma equiv-path2_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cB:G +⊢ Compositon(B)]. ∀[f:{G ⊢ _:Equiv(A;B)}].
  (equiv-path2(G;A;B;cA;cB;f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;A;B;f)))
BY
{ (Intros
   THEN (Assert ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN Unfolds ``equiv-path1 equiv-path2`` 0
   THEN InstLemma `case-type-comp-disjoint` [⌜parm{i|j}⌝;⌜parm{i}⌝;⌜G.𝕀⌝;⌜(q=0)⌝;⌜(q=1)⌝;⌜(A)p⌝;⌜(B)p⌝;⌜(cA)p⌝;⌜(cB)p⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[cB:G  +\mvdash{}  Compositon(B)].
\mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].
    (equiv-path2(G;A;B;cA;cB;f)  \mmember{}  G.\mBbbI{}  +\mvdash{}  Compositon(equiv-path1(G;A;B;f)))


By

---

Latex:
(Intros
  THEN  (Assert  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (A)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (B)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfolds  ``equiv-path1  equiv-path2``  0
  THEN  InstLemma  `case-type-comp-disjoint`  [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(q=0)\mkleeneclose{};\mkleeneopen{}(q=1)\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{}
  ;\mkleeneopen{}(cA)p\mkleeneclose{};\mkleeneopen{}(cB)p\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index