Step
*
of Lemma
permr_suptyping
∀T:Type. ∀Q:T ⟶ ℙ. ∀as,bs:{z:T| Q[z]} List. ((as ≡(T) bs)
⇒ (as ≡({z:T| Q[z]} ) bs))
BY
{ (UnivCD THENA Auto) }
1
1. T : Type
2. Q : T ⟶ ℙ
3. as : {z:T| Q[z]} List
4. bs : {z:T| Q[z]} List
5. as ≡(T) bs
⊢ as ≡({z:T| Q[z]} ) bs
Latex:
Latex:
\mforall{}T:Type. \mforall{}Q:T {}\mrightarrow{} \mBbbP{}. \mforall{}as,bs:\{z:T| Q[z]\} List. ((as \mequiv{}(T) bs) {}\mRightarrow{} (as \mequiv{}(\{z:T| Q[z]\} ) bs))
By
Latex:
(UnivCD THENA Auto)
Home
Index