Step
*
1
1
of Lemma
ifthenelse-wf
1. b : Unit?
2. A : Type
3. p : ⋂v:↑b. A
4. q : ⋂v:¬↑b. A
⊢ case b of inl() => p | inr() => q ∈ A
BY
{ ((D 1 THEN All (RepUR ``assert ifthenelse``)) THEN Reduce 0) }
1
1. x : Unit
2. A : Type
3. p : ⋂v:True. A
4. q : ⋂v:¬True. A
⊢ p ∈ A
2
1. y : Unit
2. A : Type
3. p : ⋂v:False. A
4. q : ⋂v:¬False. A
⊢ q ∈ A
Latex:
Latex:
1. b : Unit?
2. A : Type
3. p : \mcap{}v:\muparrow{}b. A
4. q : \mcap{}v:\mneg{}\muparrow{}b. A
\mvdash{} case b of inl() => p | inr() => q \mmember{} A
By
Latex:
((D 1 THEN All (RepUR ``assert ifthenelse``)) THEN Reduce 0)
Home
Index