---

Step * of Lemma awf-solution_wf

No Annotations
∀[A,I:Type].
  ∀G:awf-system{i:l}(I;A)
    (awf-solution(G) ∈ {s:I ⟶ awf(A)| 
                        (∀i:I. ((s i) = (G s i) ∈ awf(A)))
                        ∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A)))))} )
BY
{ TACTIC:(BasicUniformUnivCD Auto
          THEN (D 0 THENA Auto)
          THEN Unhide
          THEN Subst ⌜awf-solution(G) ~ TERMOF{unique-awf:o, i:l, i:l} G⌝ 0⋅) }

1
.....equality..... 
1. A : Type
2. I : Type
3. G : awf-system{i:l}(I;A)@i'
⊢ awf-solution(G) ~ TERMOF{unique-awf:o, i:l, i:l} G

2
1. A : Type
2. I : Type
3. G : awf-system{i:l}(I;A)@i'
⊢ TERMOF{unique-awf:o, i:l, i:l} G ∈ {s:I ⟶ awf(A)| 
                                      (∀i:I. ((s i) = (G s i) ∈ awf(A)))
                                      ∧ (∀s':I ⟶ awf(A)
                                           ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A)))))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,I:Type].
    \mforall{}G:awf-system\{i:l\}(I;A)
        (awf-solution(G)  \mmember{}  \{s:I  {}\mrightarrow{}  awf(A)| 
                                                (\mforall{}i:I.  ((s  i)  =  (G  s  i)))
                                                \mwedge{}  (\mforall{}s':I  {}\mrightarrow{}  awf(A).  ((\mforall{}i:I.  ((s'  i)  =  (G  s'  i)))  {}\mRightarrow{}  (s'  =  s)))\}  )


By

---

Latex:
TACTIC:(BasicUniformUnivCD  Auto
                THEN  (D  0  THENA  Auto)
                THEN  Unhide
                THEN  Subst  \mkleeneopen{}awf-solution(G)  \msim{}  TERMOF\{unique-awf:o,  i:l,  i:l\}  G\mkleeneclose{}  0\mcdot{})

---

Home Index