elim (cnv_fwd_aaa … H) -H #A #HA
/2 width=2 by cpms_total_aaa/
qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cnv_inv_appl_SO (a) (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
+ ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
+* #h #G #L #V #T #H
+elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU
+[ elim (cnv_fwd_aaa … HT) #A #HA
+ elim (aaa_cpm_SO h … (ⓛ{p}W.U))
+ [|*: /2 width=8 by cpms_aaa_conf/ ] #X #HU0
+ elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct
+ lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0
+ lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0
+ /2 width=7 by ex5_4_intro/
+| lapply (Ha ?) -Ha [ // ] #Ha
+ lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct
+ /2 width=7 by ex5_4_intro/
+| @(ex5_4_intro … HV HT HVW HTU) #H destruct
+]
+qed-.
+
+lemma cnv_inv_appl_true (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
+ ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
+ ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W0.U0.
+#h #G #L #V #T #H
+elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn
+>Hn -n [| // ] #HV #HT #HVW #HTU
+/2 width=5 by ex4_3_intro/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_equivalence/cpcs_cprs.ma".
-include "basic_2/dynamic/cnv_preserve.ma".
+include "basic_2/rt_computation/csx_aaa.ma".
+include "basic_2/rt_equivalence/cpcs_csx.ma".
+include "basic_2/dynamic/cnv_aaa.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Forward lemmas with r-equivalence ****************************************)
+(* Properties with r-equivalence ********************************************)
-lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L):
- ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
- ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
-#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2
-elim (cnv_cpms_conf … HT … HT1 … HT2) -T <minus_n_n #T #HT1 #HT2
-/2 width=3 by cprs_div/
-qed-.
-
-lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
- ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
-#a #h #G #L #V #T #H0 #n #X #HX
-elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
-elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
-lapply (cpms_appl_dx … V V … HTU) [ // ] #H
-/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+lemma cnv_cpcs_dec (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T2 ![a,h] →
+ Decidable … (⦃G,L⦄ ⊢ T1 ⬌*[h] T2).
+#a #h #G #L #T1 #HT1 #T2 #HT2
+elim (cnv_fwd_aaa … HT1) -HT1 #A1 #HA1
+elim (cnv_fwd_aaa … HT2) -HT2 #A2 #HA2
+/3 width=2 by csx_cpcs_dec, aaa_csx/
qed-.
include "basic_2/rt_computation/cpms_cpms.ma".
include "basic_2/rt_equivalence/cpes.ma".
-include "basic_2/dynamic/cnv.ma".
+include "basic_2/dynamic/cnv_aaa.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
/3 width=7 by cpms_div, ex5_4_intro/
qed-.
+lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
+ ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
+#a #h #G #L #V #T #H
+elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
+/3 width=7 by cpms_div, ex5_4_intro/
+qed-.
+
+lemma cnv_inv_appl_true_cpes (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
+ ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
+ ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
+#h #G #L #V #T #H
+elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
+>Hn -n [| // ] #HV #HT #HVW #HTU
+/2 width=5 by ex4_3_intro/
+qed-.
+
lemma cnv_inv_cast_cpes (a) (h) (G) (L):
∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ{p}W.T
- | (∀p,W,T. X = ⓛ{p}W.T → ⊥).
-* [ #I | * [ #p * | #I ] #V #T ]
-[3: /3 width=4 by ex1_3_intro, or_introl/ ]
-@or_intror #q #W #U #H destruct
-qed-.
-
(* main properties with evaluations for rt-transition on terms **************)
theorem cnv_dec (a) (h) (G) (L) (T):
[ elim HTU -HTU #HTU #_
/3 width=7 by cnv_appl_cpes, or_introl/
| @or_intror #H
- elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #HVW0
- >Hm1 -m1 [| // ] #HTU0
+ elim (cnv_inv_appl_true_cpes … H) -H #q #W0 #U0 #_ #_ #HVW0 #HTU0
elim (cnv_cpme_cpms_conf … HT … HTU0 … HTU) -T #HU0 #_
elim (cpms_inv_abst_bi … HU0) -HU0 #_ #HW0 #_ -p -q -U0
/3 width=3 by cpes_cprs_trans/
]
| #HnTU #HTX
@or_intror #H
- elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #_
- >Hm1 -m1 [| // ] #HTU0
+ elim (cnv_inv_appl_true_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0
elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_
elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0
/2 width=4 by/
[ elim HTU -HTU #n #HTU #_
@or_introl @(cnv_appl_cpes … HV … HT … HVW … HTU) #H destruct
| @or_intror #H
- elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0
+ elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0
elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX
elim (tueq_inv_bind1 … HUX) -HUX #X0 #_ #H destruct -U
elim (cpms_inv_abst_bi … HU0X) -HU0X #_ #HW0 #_ -p -q -m2 -U0 -X0
]
| #HnTU #HTX
@or_intror #H
- elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0
+ elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0
elim (cnv_cpue_cpms_conf … HT … HTU0 … HTX) -m1 -T #X0 * #m2 #HUX0 #_ #HX0
elim (cpms_inv_abst_sn … HUX0) -HUX0 #V0 #T0 #_ #_ #H destruct -m2 -W0 -U0
elim (tueq_inv_bind2 … HX0) -HX0 #X0 #_ #H destruct
]
]
@or_intror #H
- elim (cnv_inv_appl_SO … H) -H /2 width=1 by/
+ elim (cnv_inv_appl … H) -H /2 width=1 by/
| #U #T #HG #HL #HT destruct
elim (IH G L U) [| -IH | // ] #HU
[ elim (IH G L T) -IH [3: // ] #HT
#a #h #G #L1 #T #HT #L2 #H
@(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/
qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cnv_inv_appl_SO (a) (h) (G) (L):
- ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
- ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
- ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
-* #h #G #L #V #T #H
-elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU
-[ elim (cnv_fwd_cpm_SO … (ⓛ{p}W.U))
- [|*: /2 width=8 by cnv_cpms_trans/ ] #X #HU0
- elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct
- lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0
- lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0
- /2 width=7 by ex5_4_intro/
-| lapply (Ha ?) -Ha [ // ] #Ha
- lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct
- /2 width=7 by ex5_4_intro/
-| @(ex5_4_intro … HV HT HVW HTU) #H destruct
-]
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_equivalence/cpcs_cprs.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with r-equivalence ****************************************)
+
+lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+ ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2
+elim (cnv_cpms_conf … HT … HT1 … HT2) -T <minus_n_n #T #HT1 #HT2
+/2 width=3 by cprs_div/
+qed-.
+
+lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
+ ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
+#a #h #G #L #V #T #H0 #n #X #HX
+elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
+elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
+lapply (cpms_appl_dx … V V … HTU) [ // ] #H
+/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+qed-.
/3 width=6 by cpre_mono/
]
qed-.
-
-(* Advanced inversion lemmas with t-bound rt-equivalence for terms **********)
-
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
- ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
- ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
- ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/cnv_eval.ma".
+include "basic_2/dynamic/nta_preserve.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* Properties with evaluations for rt-transition on terms *******************)
+
+lemma nta_typecheck_dec (a) (h) (G) (L):
+ ∀T,U. Decidable … (⦃G,L⦄ ⊢ T :[a,h] U).
+/2 width=1 by cnv_dec/ qed-.
+
+(* Basic_1: uses: ty3_inference *)
+lemma nta_inference_dec (a) (h) (G) (L) (T):
+ ∨∨ ∃U. ⦃G,L⦄ ⊢ T :[a,h] U
+ | ∀U. (⦃G,L⦄ ⊢ T :[a,h] U → ⊥).
+#a #h #G #L #T
+elim (cnv_dec a h G L T)
+[ /3 width=1 by cnv_nta_sn, or_introl/
+| /4 width=2 by nta_fwd_cnv_sn, or_intror/
+]
+qed-.
(**************************************************************************)
include "basic_2/rt_equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/cnv_cpcs.ma".
+include "basic_2/dynamic/cnv_preserve_cpcs.ma".
include "basic_2/dynamic/nta.ma".
(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h].
#h #G #L #X2 #V #T #H
elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2
-elim (cnv_inv_appl … H1) * [ | #n ] #p #W #U #Hn #HV #HT #HVW #HTU
-[ lapply (cnv_cpms_trans … HT … HTU) #H
- elim (cnv_inv_bind … H) -H #_ #HU
- elim (cnv_fwd_cpm_SO … HU) #U0 #HU0 -HU
- lapply (cpms_step_dx … HTU 1 (ⓛ{p}W.U0) ?) -HTU [ /2 width=1 by cpm_bind/ ] #HTU
-| lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Hn #H destruct
-]
+elim (cnv_inv_appl_true … H1) #p #W #U #HV #HT #HVW #HTU
/5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/
qed-.
(* Basic_1: uses: ty3_gen_abst_abst *)
lemma nta_inv_abst_bi
+(* Basic_1: uses: pc3_dec *)
+lemma nta_cpcs_dec
+
(* Advanced properties ******************************************************)
| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
--- /dev/null
+(* FROM BASIC_1
+
+(* NOTE: This can be generalized removing the last premise *)
+ Lemma ty3_gen_cvoid: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
+ (e:?; u:?; d:?) (getl d c (CHead e (Bind Void) u)) ->
+ (a:?) (drop (1) d c a) ->
+ (EX y1 y2 | t1 = (lift (1) d y1) &
+ t2 = (lift (1) d y2) &
+ (ty3 g a y1 y2)
+ ).
+
+Lemma ty3_gen_appl_nf2: (g:?; c:?; w,v,x:?) (ty3 g c (THead (Flat Appl) w v) x) ->
+ (EX u t | (pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x) &
+ (ty3 g c v (THead (Bind Abst) u t)) &
+ (ty3 g c w u) &
+ (nf2 c (THead (Bind Abst) u t))
+ ).
+
+Lemma ty3_arity: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
+ (EX a1 | (arity g c t1 a1) &
+ (arity g c t2 (asucc g a1))
+ ).
+
+Lemma ty3_acyclic: (g:?; c:?; t,u:?)
+ (ty3 g c t u) -> (pc3 c u t) -> (P:Prop) P.
+
+Theorem pc3_abst_dec: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
+ (u2,t2:?) (ty3 g c u2 t2) ->
+ (EX u v2 | (pc3 c u1 (THead (Bind Abst) u2 u)) &
+ (ty3 g c (THead (Bind Abst) v2 u) t1) &
+ (pr3 c u2 v2) & (nf2 c v2)
+ ) \/
+ ((u:?) (pc3 c u1 (THead (Bind Abst) u2 u)) -> False).
+
+file ty3_nf2_gen
+
+*)
class "magenta"
[ { "dynamic typing" * } {
[ { "context-sensitive native type assignment" * } {
- [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" * ]
+ [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" + "nta_eval" * ]
}
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpue" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpue" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
}
]
}
(* Basic properties *********************************************************)
+lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ{p}W.T
+ | (∀p,W,T. X = ⓛ{p}W.T → ⊥).
+* [ #I | * [ #p * | #I ] #V #T ]
+[3: /3 width=4 by ex1_3_intro, or_introl/ ]
+@or_intror #q #W #U #H destruct
+qed-.
+
(* Basic_1: was: term_dec *)
lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]