---

Step * 2 1 3 1 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
6. x : {a:Id| (a ∈ A)} 
⊢ (x1 x) = (y1 x) ∈ (ℤ × j:ℤ fp-> V)
BY
{ ((InstHyp [⌈x⌉] (-2)⋅ THENA Auto) THEN MoveToConcl (-1)) }

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)} 
⊢ (((fst((y1 x))) = (fst((x1 x))) ∈ ℤ) ∧ ((snd((y1 x))) = (snd((x1 x))) ∈ i:ℤ fp-> V))
⇒ ((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
6.  x  :  \{a:Id|  (a  \mmember{}  A)\} 
\mvdash{}  (x1  x)  =  (y1  x)


By

((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1))

---

Home Index