Step
*
of Lemma
strong-subtype-set3
∀[A,B:Type]. ∀[P:A ⟶ ℙ]. strong-subtype({x:A| P[x]} ;B) supposing strong-subtype(A;B)
BY
{ (((Auto THEN (InstLemma `strong-subtype-set` [⌜A⌝; ⌜B⌝; ⌜P⌝; ⌜λx.True⌝])⋅) THENA Auto)
THEN ReduceSOAps 0
THEN Auto
THEN (InstLemma `strong-subtype-set2` [⌜B⌝; ⌜λx.True⌝])⋅
THEN Auto) }
1
1. A : Type
2. B : Type
3. P : A ⟶ ℙ
4. strong-subtype(A;B)
5. strong-subtype({x:A| P[x]} ;{x:B| λx.True[x]} )
6. strong-subtype({x:B| λx.True[x]} ;B)
⊢ strong-subtype({x:A| P x} ;B)
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[P:A {}\mrightarrow{} \mBbbP{}]. strong-subtype(\{x:A| P[x]\} ;B) supposing strong-subtype(A;B)
By
Latex:
(((Auto THEN (InstLemma `strong-subtype-set` [\mkleeneopen{}A\mkleeneclose{}; \mkleeneopen{}B\mkleeneclose{}; \mkleeneopen{}P\mkleeneclose{}; \mkleeneopen{}\mlambda{}x.True\mkleeneclose{}])\mcdot{}) THENA Auto)
THEN ReduceSOAps 0
THEN Auto
THEN (InstLemma `strong-subtype-set2` [\mkleeneopen{}B\mkleeneclose{}; \mkleeneopen{}\mlambda{}x.True\mkleeneclose{}])\mcdot{}
THEN Auto)
Home
Index