Step
*
1
1
1
of Lemma
face-map_wf2
1. I : Cname List
2. x : Cname
3. p : ℕ2
4. x@0 : Cname@i
5. (x@0 ∈ I)@i
⊢ (x@0 = x ∈ Cname) ∨ ((x@0 ∈ I) ∧ (¬(x@0 = x ∈ Cname)))
BY
{ (Decide x@0 = x ∈ Cname THEN Auto) }
Latex:
Latex:
1. I : Cname List
2. x : Cname
3. p : \mBbbN{}2
4. x@0 : Cname@i
5. (x@0 \mmember{} I)@i
\mvdash{} (x@0 = x) \mvee{} ((x@0 \mmember{} I) \mwedge{} (\mneg{}(x@0 = x)))
By
Latex:
(Decide x@0 = x THEN Auto)
Home
Index