---

Step * of Lemma name-morph-flip-flip

∀I:Cname List. ∀f:name-morph(I;[]). ∀j:nameset(I).  (flip(flip(f;j);j) = f ∈ name-morph(I;[]))
BY
{ ((Auto THEN BLemma `name-morph-ext` THEN Auto)
   THEN RepUR ``name-morph-flip`` 0
   THEN (BoolCase ⌜eq-cname(x;j)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. f : name-morph(I;[])
3. j : nameset(I)
4. x : nameset(I)
5. x = j ∈ Cname
⊢ (1 - 1 - f x) = (f x) ∈ extd-nameset([])

2
1. I : Cname List
2. f : name-morph(I;[])
3. j : nameset(I)
4. x : nameset(I)
5. ¬(x = j ∈ Cname)
⊢ (f x) = (f x) ∈ extd-nameset([])

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}f:name-morph(I;[]).  \mforall{}j:nameset(I).    (flip(flip(f;j);j)  =  f)


By

---

Latex:
((Auto  THEN  BLemma  `name-morph-ext`  THEN  Auto)
  THEN  RepUR  ``name-morph-flip``  0
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x;j)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index