---

Step * 2 1 3 1 1 1 of Lemma consensus-refinement4


1. V : Type@i'
2. A : Id List@i
3. x1 : {a:Id| (a ∈ A)}  ─→ (ℤ × j:ℤ fp-> V)@i
4. y1 : {a:Id| (a ∈ A)}  ─→ (ℤ × j:ℤ fp-> V)@i
5. ∀b:{a:Id| (a ∈ A)} . (((fst((y1 b))) = (fst((x1 b))) ∈ ℤ) ∧ ((snd((y1 b))) = (snd((x1 b))) ∈ i:ℤ fp-> V))@i
⊢ x1 = y1 ∈ ({a:Id| (a ∈ A)}  ─→ (ℤ × j:ℤ fp-> V))
BY
{ (Ext THEN Auto) }

1
1. V : Type@i'
2. A : Id List@i
3. x1 : {a:Id| (a ∈ A)}  ─→ (ℤ × j:ℤ fp-> V)@i
4. y1 : {a:Id| (a ∈ A)}  ─→ (ℤ × j:ℤ fp-> V)@i
5. ∀b:{a:Id| (a ∈ A)} . (((fst((y1 b))) = (fst((x1 b))) ∈ ℤ) ∧ ((snd((y1 b))) = (snd((x1 b))) ∈ i:ℤ fp-> V))@i
6. x : {a:Id| (a ∈ A)} 
⊢ (x1 x) = (y1 x) ∈ (ℤ × j:ℤ fp-> V)

---

Latex:



1.  V  :  Type@i'
2.  A  :  Id  List@i
3.  x1  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  j:\mBbbZ{}  fp->  V)@i
4.  y1  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  j:\mBbbZ{}  fp->  V)@i
5.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (((fst((y1  b)))  =  (fst((x1  b))))  \mwedge{}  ((snd((y1  b)))  =  (snd((x1  b)))))@i
\mvdash{}  x1  =  y1


By

(Ext  THEN  Auto)

---

Home Index