equal
deleted
inserted
replaced
145 |
145 |
146 (* type extensionality - needed in order to get the soundness theorem through*) |
146 (* type extensionality - needed in order to get the soundness theorem through*) |
147 | tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; |
147 | tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; |
148 \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K" |
148 \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K" |
149 |
149 |
150 thm sig_valid_ctx_valid_trm_valid_ty_valid_kind_valid_trm_equiv_ty_equiv_kind_equiv_def |
|
151 thm sig_valid_def |
|
152 thm trm_valid_def |
|
153 thm ty_valid_def |
|
154 thm kind_valid_def |
|
155 thm trm_equiv_def |
|
156 thm kind_equiv_def |
|
157 thm ty_equiv_def |
|
158 |
150 |
159 end |
151 end |
160 |
152 |
161 |
153 |
162 |
154 |