Step
*
1
of Lemma
per-close_wf
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)) ⟶ 𝕌')
BY
{ Auto }
Latex:
Latex:
1. Term : Type
2. Term \msubseteq{}r Base
3. EQ : Term {}\mrightarrow{} Term {}\mrightarrow{} Term {}\mrightarrow{} 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) \mtimes{} Term \mtimes{} Term \mtimes{} term-equality\{i:l\}(Term)) {}\mrightarrow{} \mBbbU{}'
\mvdash{} (\mlambda{}p.let ts,T,T',eq = p
in (ts T T' eq) \mvee{} per-eq-def\{i:l\}(Term;EQ;\mlambda{}T,T',eq. (x <ts, T, T', eq>);T;T';eq) )
= (\mlambda{}p.let ts,T,T',eq = p
in (ts T T' eq) \mvee{} per-eq-def\{i:l\}(Term;EQ;\mlambda{}T,T',eq. (x <ts, T, T', eq>);T;T';eq) )
By
Latex:
Auto
Home
Index