Step * of Lemma compact-union

[T,S:Type].  (compact-type(T)  compact-type(S)  compact-type(T S))
BY
(Auto THEN All (Unfold `compact-type`)⋅ THEN THEN Auto) }

1
1. [T] Type
2. [S] Type
3. ∀p:T ⟶ 𝔹((∃x:T. ff) ∨ (∀x:T. tt))
4. ∀p:S ⟶ 𝔹((∃x:S. ff) ∨ (∀x:S. tt))
5. (T S) ⟶ 𝔹
⊢ (∃x:T S. ff) ∨ (∀x:T S. tt)


Latex:


Latex:
\mforall{}[T,S:Type].    (compact-type(T)  {}\mRightarrow{}  compact-type(S)  {}\mRightarrow{}  compact-type(T  +  S))


By


Latex:
(Auto  THEN  All  (Unfold  `compact-type`)\mcdot{}  THEN  D  0  THEN  Auto)




Home Index