---

Step * of Lemma per-close_wf

No Annotations
∀[Term:{T:Type| T ⊆r Base} ]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i:l}(Term)].
∀[T,T':Term]. ∀[eq:term-equality{i:l}(Term)].
  (per-close{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌')
BY
{ (ProveWfLemma THEN Unfold `member` 0 THEN Refine_parameterizedRecEquality `x' `y' `z' `c'⋅) }

1
1. Term : Type
2. Term ⊆r Base
3. EQ : Term ⟶ Term ⟶ Term ⟶ Term
4. ts : candidate-type-system{i:l, i:l}(Term)
5. T : Term
6. T' : Term
7. eq : term-equality{i:l}(Term)
8. x : (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term)) ⟶ 𝕌'
⊢ (λp.let ts,T,T',eq = p 
      in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (x <ts, T, T', eq>);T;T';eq)  )
= (λp.let ts,T,T',eq = p 
      in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (x <ts, T, T', eq>);T;T';eq)  )
∈ ((candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term)) ⟶ 𝕌')

2
1. Term : Type
2. Term ⊆r Base
3. EQ : Term ⟶ Term ⟶ Term ⟶ Term
4. ts : candidate-type-system{i:l, i:l}(Term)
5. T : Term
6. T' : Term
7. eq : term-equality{i:l}(Term)
8. x : (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term)) ⟶ 𝕌'
9. y : (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term)) ⟶ 𝕌'
10. z : ∀c:candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term). ((x c) ⊆r (y c))
⊢ ∀c:candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term)
    (((λp.let ts,T,T',eq = p in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (x <ts, T, T', eq>);T;T';eq)  ) c)
       ⊆r ((λp.let ts,T,T',eq = p in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (y <ts, T, T', eq>);T;T';eq)  ) c)\000C)

3
1. Term : Type
2. Term ⊆r Base
3. EQ : Term ⟶ Term ⟶ Term ⟶ Term
4. ts : candidate-type-system{i:l, i:l}(Term)
5. T : Term
6. T' : Term
7. eq : term-equality{i:l}(Term)
⊢ (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term))
= (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term))
∈ 𝕌'

4
1. Term : Type
2. Term ⊆r Base
3. EQ : Term ⟶ Term ⟶ Term ⟶ Term
4. ts : candidate-type-system{i:l, i:l}(Term)
5. T : Term
6. T' : Term
7. eq : term-equality{i:l}(Term)
⊢ <ts, T, T', eq> = <ts, T, T', eq> ∈ (candidate-type-system{i:l, i:l}(Term) × Term × Term × term-equality{i:l}(Term))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Term:\{T:Type|  T  \msubseteq{}r  Base\}  ].  \mforall{}[EQ:Term  {}\mrightarrow{}  Term  {}\mrightarrow{}  Term  {}\mrightarrow{}  Term].  \mforall{}[ts:candidate-type-system\{i:l,
                                                                                                                                                                                          i:l\}
                                                                                                                                                  (Term)].  \mforall{}[T,T':Term].
\mforall{}[eq:term-equality\{i:l\}(Term)].
    (per-close\{i:l\}(Term;EQ;ts;T;T';eq)  \mmember{}  \mBbbU{}')


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `member`  0  THEN  Refine\_parameterizedRecEquality  `x'  `y'  `z'  `c'\mcdot{})

---

Home Index