(* Basic_1: was by definition: pr2_free *)
lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
-/2/ qed.
+/2 width=3/ qed.
lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2.
/3 width=5/ qed.
lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
-/2/ qed.
+/2 width=1/ qed.
(* Note: new property *)
(* Basic_1: was only: pr2_thin_dx *)
lemma cpr_cast: ∀L,V,T1,T2.
L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
-#L #V #T1 #T2 * /3/
+#L #V #T1 #T2 * /3 width=3/
qed.
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 →
∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/
+lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
(* Basic inversion lemmas ***************************************************)
U2 = 𝕔{Cast} V2. T2
) ∨ L ⊢ T1 ⇒ U2.
#L #V1 #T1 #U2 * #X #H #HU2
-elim (tpr_inv_cast1 … H) -H /3/
-* #V #T #HV1 #HT1 #H destruct -X;
-elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
+elim (tpr_inv_cast1 … H) -H /3 width=3/
+* #V #T #HV1 #HT1 #H destruct
+elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
qed-.
(* Basic_1: removed theorems 5:
lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
-@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
+@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
qed.
(* Basic_1: was only: pr2_gen_cbind *)
L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2 width=1/ #HT0
lapply (tpss_tps … HT0) -HT0 #HT0
-@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
+@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
(* Advanced forward lemmas **************************************************)
i < |L|.
#L #T2 #i * #X #H
>(tpr_inv_atom1 … H) -H #H
-elim (tpss_inv_lref1 … H) -H /2/
+elim (tpss_inv_lref1 … H) -H /2 width=1/
* /3 width=6/
qed-.
(* Basic_1: was: pr2_gen_abst *)
lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ qed-.
+/2 width=3/ qed-.
(* Relocation properties ****************************************************)
elim (lift_total T d e) #U #HTU
lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
elim (lt_or_ge (|K|) d) #HKd
-[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ]
-| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/
+[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ]
+| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/
]
qed.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ]
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ]
| elim (lt_or_ge (|L|) (d + e)) #HLde
- [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ]
- | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/
+ [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ]
+ | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/
]
]
qed.
∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
-elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU
-elim (tpss_conf_eq … HT2 … HTU) -T /3/
+elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
+elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/
qed.
lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 →
∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
->(ltpr_fwd_length … HL12) in HT2 #HT2
-elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/
+>(ltpr_fwd_length … HL12) in HT2; #HT2
+elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/
qed.
lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 →
∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2.
#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
-elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2
+elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2
lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
qed.
(* Basic properties *********************************************************)
lemma lcpr_refl: ∀L. L ⊢ ⇒ L.
-/2/ qed.
+/2 width=3/ qed.
(* Basic inversion lemmas ***************************************************)
(* Basic properties *********************************************************)
lemma ltpr_refl: ∀L:lenv. L ⇒ L.
-#L elim L -L /2/
+#L elim L -L // /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
[ //
| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
]
(* Basic_1: was: wcpr0_gen_sort *)
lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
-/2/ qed-.
+/2 width=3/ qed-.
fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
]
qed.
(* Basic_1: was: wcpr0_gen_head *)
lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-/2/ qed-.
+/2 width=3/ qed-.
fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
[ //
| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
]
qed.
lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆.
-/2/ qed-.
+/2 width=3/ qed-.
fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
[ #K2 #I #V2 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
]
qed.
lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-/2/ qed-.
+/2 width=3/ qed-.
(* Basic forward lemmas *****************************************************)
lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
-#L1 #L2 #H elim H -H L1 L2; normalize //
+#L1 #L2 #H elim H -L1 -L2 normalize //
qed-.
(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
(* Basic_1: was: wcpr0_ldrop *)
lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 →
∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
| #K1 #I #V1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
- elim (IHLK1 … HL12) -IHLK1 HL12 /3/
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 /3 width=3/
| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
- elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1;
- elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (tpr_inv_lift … HV12 … HWV1) -V1
+ elim (IHLK1 … HL12) -L1 /3 width=5/
]
qed.
(* Basic_1: was: wcpr0_ldrop_back *)
lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 →
∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
| #K1 #I #V1 #X #H
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+ elim (IHLK1 … HK12) -K1 /3 width=5/
| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X;
+ elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
elim (lift_total W2 d e) #V2 #HWV2
- lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1;
- elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+ lapply (tpr_lift … HW12 … HWV1 … HWV2) -W1
+ elim (IHLK1 … HK12) -K1 /3 width=5/
]
qed.
lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T].
#V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
-| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
+[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
]
qed-.
lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
#V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
-| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
-| generalize in match HVT1 -HVT1; elim T1 -T1 * // * #W1 #U1 #_ #_ #H
+[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct
- | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct
+ lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2 width=3/ -HV12 #H destruct
+ | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2 width=1/ #H destruct
]
qed-.
lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
- lapply (H U ?) -H /2 width=3/ #H destruct -U;
+ lapply (H U ?) -H /2 width=3/ #H destruct
elim (lift_inv_pair_xy_y … HTU)
| #HT
elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12
- lapply (H (𝕓{Abbr}V.T2) ?) -H /2/ -HT2 #H destruct -T /3 width=2/
+ lapply (H (𝕓{Abbr}V.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
]
qed.
(* Basic properties *********************************************************)
lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2.
-#T1 #T2 #H elim H -T1 T2
+#T1 #T2 #H elim H -T1 -T2
[ //
| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
[ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
elim (tif_inv_appl … H) -H #_ #_ #H
elim (simple_inv_bind … H)
| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
- [ -HT2 IHV1 IHT1; elim (tif_inv_abbr … H)
+ [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
| <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
elim (tif_inv_abst … H) -H #HV1 #HT1
>IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
qed.
theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1].
-/2/ qed.
+/2 width=1/ qed.
(* Note: this property is unusual *)
theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
#T1 #H elim H -T1
-[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2/
-| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
+[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
| #V #T #H elim (tnf_inv_abbr … H)
| #V #T #H elim (tnf_inv_cast … H)
| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
qed.
theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
-/2/ qed.
+/2 width=3/ qed.
lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T].
/4 width=1/ qed.
lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-/2/ qed.
+/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
lemma tpr_refl: ∀T. T ⇒ T.
#T elim T -T //
-#I elim I -I /2/
+#I elim I -I /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ //
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
-/2/ qed-.
+/2 width=3/ qed-.
fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
(∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
U2 = 𝕓{I} V2. T
) ∨
∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ #J #I #V #T #H destruct
| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
]
qed.
U2 = 𝕓{I} V2. T
) ∨
∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-/2/ qed-.
+/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
I = Appl
| (U0 ⇒ U2 ∧ I = Cast).
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ #I #J #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
- destruct -J V1 T0 /3 width=12/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
]
qed.
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
I = Appl
| (U0 ⇒ U2 ∧ I = Cast).
-/2/ qed-.
+/2 width=3/ qed-.
(* Basic_1: was pr0_gen_appl *)
lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
#V1 #T1 #U #H #HT1
elim (tpr_inv_appl1 … H) -H *
[ /2 width=5/
-| #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1;
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct
elim (simple_inv_bind … HT1)
-| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1;
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
elim (simple_inv_bind … HT1)
]
qed-.
| ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #I #i #H destruct /2/
+#T1 #T2 * -T1 -T2
+[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
+| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
]
qed.
| ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
-/2/ qed-.
+/2 width=3/ qed-.
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
(* Basic_1: was: pr0_lift *)
lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
[ * #i #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
- [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
- | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
- | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 //
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct
+ [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct //
+ | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct //
+ | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct //
]
| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
- elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
+ elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
+ elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/
| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
- elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
+ elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/
| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
+ elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
+ elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct
elim (lift_total T2 (d + 1) e) #U2 #HTU2
@tpr_delta
- [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *)
+ [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
- elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
- elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
- elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
+ elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
+ elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
+ elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/
| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
- elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
- elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/
+ elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct
+ elim (lift_trans_ge … HT1 … HT3 ?) -T // /3 width=6/
| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
- elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/
+ elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/
]
qed.
lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
∀d,e,U1. ↑[d, e] U1 ≡ T1 →
∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
[ * #i #d #e #U1 #HU1
- [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
- | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
- | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/
+ [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
+ | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct /3 width=3/
+ | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct /2 width=3/
]
| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
- elim (IHV12 … HV01) -IHV12 HV01;
- elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct
+ elim (IHV12 … HV01) -V1
+ elim (IHT12 … HT01) -T1 /3 width=5/
| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
- elim (IHV12 … HV01) -IHV12 HV01;
- elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+ elim (IHV12 … HV01) -V1
+ elim (IHT12 … HT01) -T1 /3 width=5/
| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
- elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
- elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
- elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
- @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *)
+ elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct
+ elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
+ elim (IHT12 … HUT1) -T1 #U2 #HUT2 #HU12
+ elim (tps_inv_lift1_le … HT20 … HUT2 ?) -T2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+ @ex2_1_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
- elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03
- elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03
- elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03
- elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
- @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *)
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+ elim (IHV12 … HV01) -V1 #V3 #HV32 #HV03
+ elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03
+ elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
+ elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
+ @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
- elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
- elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
- elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/
+ elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct
+ elim (lift_div_le … HT1 … HT0 ?) -T // #T #HT0 #HT1
+ elim (IHT12 … HT1) -T1 /3 width=5/
| #V #T1 #T2 #_ #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
- elim (IHT12 … HT01) -IHT12 HT01 /3/
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct
+ elim (IHT12 … HT01) -T1 /3 width=3/
]
qed.
fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ #I #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
- <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/
+| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct
+ <(tps_inv_refl_SO2 … HT2 ? ? ?) -T /2 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
| #V #T1 #T2 #_ #V0 #T0 #H destruct
(* Basic_1: was pr0_gen_abst *)
lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ qed-.
+/2 width=3/ qed-.
(* Confluence lemmas ********************************************************)
fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X.
-/2/ qed.
+/2 width=3/ qed.
fact tpr_conf_flat_flat:
∀I,V0,V1,T0,T1,V2,T2. (
V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0.
#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
qed.
fact tpr_conf_flat_beta:
U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 →
∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
-elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
+elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/
qed.
(* basic-1: was:
W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 →
∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
-elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2
elim (lift_total VV 0 1) #VVV #HVV
lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
elim (tpr_inv_abbr1 … H) -H *
(* case 1: delta *)
-[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
- elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
- elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
- elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
+[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
+ elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2
+ elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2
+ elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
@ex2_1_intro
[2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
|1:skip
|3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
] (**) (* /5 width=14/ is too slow *)
(* case 3: zeta *)
-| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
+| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
lapply (tw_lift … HUU10) -HUU10 #HUU10
- elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
+ elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2
@ex2_1_intro
[2: @tpr_flat
|1: skip
V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 →
∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X.
#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/
qed.
fact tpr_conf_beta_beta:
V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 //
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 //
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
qed.
(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 →
∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X.
#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
-elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
-elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
+elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
+elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
+elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
-lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1;
+lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
+elim (IH … HTX2 … HTT2) -HTX2 -HTT2 -IH // /3 width=3/
qed.
(* Basic_1: was: pr0_upsilon_upsilon *)
↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
elim (lift_total V 0 1) #VV #HVV
-lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1
-lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2
+lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1
+lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2
@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
qed.
↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 →
∃∃X. T1 ⇒ X & X2 ⇒ X.
#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
-lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0;
+lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct
lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/
+elim (IH … HT01 … HTX2) -HT01 -HTX2 -IH // /2 width=3/
qed.
fact tpr_conf_tau_tau:
T0 ⇒ T1 → T0 ⇒ X2 →
∃∃X. T1 ⇒ X & X2 ⇒ X.
#V0 #T0 #X2 #T1 #IH #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /2/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /2 width=3/
qed.
(* Confluence ***************************************************************)
) →
∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
∃∃X. X1 ⇒ X & X2 ⇒ X.
-#Y0 #IH #X0 #X1 #X2 * -X0 X1
-[ #I1 #H1 #H2 destruct -Y0;
+#Y0 #IH #X0 #X1 #X2 * -X0 -X1
+[ #I1 #H1 #H2 destruct
lapply (tpr_inv_atom1 … H1) -H1
(* case 1: atom, atom *)
- #H1 destruct -X2 //
-| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+ #H1 destruct //
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
elim (tpr_inv_flat1 … H1) -H1 *
(* case 2: flat, flat *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ [ #V2 #T2 #HV02 #HT02 #H destruct
/3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
(* case 3: flat, beta *)
- | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
+ | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct
/3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
(* case 4: flat, theta *)
- | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
+ | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct
/3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
(* case 5: flat, tau *)
- | #HT02 #H destruct -I
+ | #HT02 #H destruct
/3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
]
-| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
elim (tpr_inv_appl1 … H1) -H1 *
(* case 6: beta, flat (repeated) *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ [ #V2 #T2 #HV02 #HT02 #H destruct
@ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
(* case 7: beta, beta *)
- | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
+ | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct
/3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
(* case 8, beta, theta (excluded) *)
| #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
]
-| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
+| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct
elim (tpr_inv_bind1 … H1) -H1 *
(* case 9: delta, delta *)
- [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+ [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
/3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
(* case 10: delta, zata *)
- | #T2 #HT20 #HTX2 #H destruct -I1;
+ | #T2 #HT20 #HTX2 #H destruct
/3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
]
-| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0;
+| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct
elim (tpr_inv_appl1 … H1) -H1 *
(* case 11: theta, flat (repeated) *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ [ #V2 #T2 #HV02 #HT02 #H destruct
@ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
(* case 12: theta, beta (repeated) *)
| #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
(* case 13: theta, theta *)
- | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
+ | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct
/3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
]
-| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct
elim (tpr_inv_abbr1 … H1) -H1 *
(* case 14: zeta, delta (repeated) *)
- [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+ [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
@ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
(* case 15: zeta, zeta *)
| #T2 #HTT20 #HTX2
/3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
]
-| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #T0 #T1 #HT01 #H1 #H2 destruct
elim (tpr_inv_cast1 … H1) -H1
(* case 16: tau, flat (repeated) *)
- [ * #V2 #T2 #HV02 #HT02 #H destruct -X2
+ [ * #V2 #T2 #HV02 #HT02 #H destruct
@ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
(* case 17: tau, tau *)
| #HT02
∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
∀L2. L1 ⇒ L2 →
∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
[ #I #L1 #d #e #X #H
elim (tps_inv_atom1 … H) -H
- [ #H destruct -X /2/
- | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
- elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
+ [ #H destruct /2 width=3/
+ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct
+ elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H
+ elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct
elim (lift_total V2 0 (i+1)) #U2 #HVU2
- lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
- @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
+ lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 #HU12
+ @ex2_1_intro [2: @HU12 | skip | /3 width=4/ ] (**) (* /4 width=6/ is too slow *)
]
| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
- elim (IHV12 … HVW1 … HL12) -IHV12 HVW1;
- elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/
+ elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV12 … HVW1 … HL12) -V1
+ elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/
| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
- elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+ elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
+ elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+ elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
- lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
- elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
- lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+ elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+ elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+ elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
+ lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+ elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
+ lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
- lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
- lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
+ lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+ lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
- elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
- elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+ elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
+ elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+ elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
+ elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
elim (lift_total VV2 0 1) #VV #H2VV
- lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
+ lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
@ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
- elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
- elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
+| #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
+ elim (tps_inv_lift1_ge … HTT12 L1 … HTT1 ?) -TT1 /2 width=1/ #T2 #HT12 #HTT2
+ elim (IHT12 … HT12 … HL12) -T1 -HL12 <minus_plus_m_m /3 width=3/
| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
- elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
+ elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+ elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
]
qed.
⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -T1 /2 width=1/ /3 width=3/
qed.
lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
-[ /2/
+[ /2 width=3/
| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
- elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
- lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
+ elim (tpr_tps_ltpr … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
+ lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
]
qed.
qed.
lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
-/2/ qed-.
+/2 width=4/ qed-.
fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
#W #U #T * -T
-[ #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+[ #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
| #V #T #_ #H destruct
| #V #T #_ #H destruct
| #V #T #H destruct
qed.
lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
-/2/ qed-.
+/2 width=3/ qed-.
fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U →
∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
#W #U #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
-| #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+| #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
| #V #T #H destruct
| #V #T #H destruct
-| #V #W0 #T #H destruct -V U
+| #V #W0 #T #H destruct
@or3_intro2 #H elim (simple_inv_bind … H)
]
qed.
lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
-/2/ qed-.
+/2 width=3/ qed-.
lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
-/2/ qed-.
+/2 width=1/ qed-.
lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
-/4/ qed-.
+/4 width=1/ qed-.
lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
-#V #T #HVT @and3_intro /3/
-generalize in match HVT -HVT; elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2/
+#V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
-/2/ qed-.
+/2 width=1/ qed-.
(* Basic properties *********************************************************)
lemma tif_atom: ∀I. 𝕀[𝕒{I}].
-/2/ qed.
+/2 width=4/ qed.
lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[𝕔 {Abst}V.T].
#V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2/
+elim (trf_inv_abst … H) -H /2 width=1/
qed.
lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[𝕔{Appl}V.T].
#V #T #HV #HT #S #H
-elim (trf_inv_appl … H) -H /2/
+elim (trf_inv_appl … H) -H /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
lemma twhnf_inv_thom: ∀T. 𝕎ℍℕ[T] → T ≈ T.
-normalize /2 depth=1/
+normalize /2 width=1/
qed-.
(* Basic properties *********************************************************)
lemma tpr_thom: ∀T1,T2. T1 ⇒ T2 → T1 ≈ T1 → T1 ≈ T2.
-#T1 #T2 #H elim H -T1 T2 //
+#T1 #T2 #H elim H -T1 -T2 //
[ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
- elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct -I T1 V1;
- lapply (IHT12 HT1U2) -IHT12 HT1U2 #HUT2
+ elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
+ lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
lapply (simple_thom_repl_dx … HUT2 HT1) /2 width=1/
| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #H
elim (simple_inv_bind … H)
| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
- elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct -I //
+ elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct //
| #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
elim (thom_inv_flat1 … H) -H #U1 #U2 #_ #H
elim (simple_inv_bind … H)
qed.
lemma twhnf_thom: ∀T. T ≈ T → 𝕎ℍℕ[T].
-/2/ qed.
+/2 width=1/ qed.
projects / helm.git / commitdiff