Step
*
1
1
1
1
1
of Lemma
decidable__atom_equal_1
1. a : Atom1@i
2. b : Atom1@i
3. v : (a = b ∈ Atom1) ⟶ Void
4. x : a = b ∈ Atom1@i
⊢ {x ∈ Void}
BY
{ D (-2) THEN Auto }
Latex:
Latex:
1. a : Atom1@i
2. b : Atom1@i
3. v : (a = b) {}\mrightarrow{} Void
4. x : a = b@i
\mvdash{} \{x \mmember{} Void\}
By
Latex:
D (-2) THEN Auto
Home
Index