---

Step * of Lemma name-morph-inv-eq

∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:nameset(I)].
  (name-morph-inv(I;f) (f x)) = x ∈ nameset(I) supposing ↑isname(f x)
BY
{ TACTIC:((Auto THEN Unfold `name-morph-inv` 0)
          THEN Reduce 0
          THEN (FLemma `assert-isname` [-1] THENA Auto)
          THEN (Assert λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹 BY
                      (Auto THEN ((FLemma `assert-isname` [-1] THEN Auto) ORELSE (Unfold `nameset` 0 THEN Auto))))) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : nameset(I)
5. ↑isname(f x)
6. f x ∈ nameset(J)
7. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
⊢ hd(filter(λi.(isname(f i) ∧b (f i =z f x));I)) = x ∈ nameset(I)

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[x:nameset(I)].
    (name-morph-inv(I;f)  (f  x))  =  x  supposing  \muparrow{}isname(f  x)


By

---

Latex:
TACTIC:((Auto  THEN  Unfold  `name-morph-inv`  0)
                THEN  Reduce  0
                THEN  (FLemma  `assert-isname`  [-1]  THENA  Auto)
                THEN  (Assert  \mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x))  \mmember{}  nameset(I)  {}\mrightarrow{}  \mBbbB{}  BY
                                        (Auto
                                          THEN  ((FLemma  `assert-isname`  [-1]  THEN  Auto)
                                                    ORELSE  (Unfold  `nameset`  0  THEN  Auto)
                                                    )
                                          )))

---

Home Index