(* *)
(**************************************************************************)
-include "Basic-2/grammar/cl_weight.ma".
+include "Basic-2/grammar/lenv.ma".
(* SHIFT OF A CLOSURE *******************************************************)
].
interpretation "shift (closure)" 'Append L T = (shift L T).
-
-(* Basic properties *********************************************************)
-
-lemma tw_shift: βL,T. #[L, T] β€ #[L @ T].
-#L elim L //
-#K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2/ | skip ]
-qed.
-
-
(**************************************************************************)
include "Basic-2/grammar/lenv_weight.ma".
+include "Basic-2/grammar/cl_shift.ma".
(* WEIGHT OF A CLOSURE ******************************************************)
(* Basic properties *********************************************************)
-lemma cw_shift: βK,I,V,T. #[K. π{I} V, T] < #[K, π{I} V. T].
-normalize //
-qed.
-
axiom cw_wf_ind: βR:lenvβtermβProp.
(βL2,T2. (βL1,T1. #[L1,T1] < #[L2,T2] β R L1 T1) β R L2 T2) β
βL,T. R L T.
+
+lemma cw_shift: βK,I,V,T. #[K. π{I} V, T] < #[K, π{I} V. T].
+normalize //
+qed.
+
+lemma tw_shift: βL,T. #[L, T] β€ #[L @ T].
+#L elim L //
+#K #I #V #IHL #T
+@transitive_le [3: @IHL |2: /2/ | skip ]
+qed.
include "Ground-2/list.ma".
include "Basic-2/notation.ma".
-(* BINARY ITEMS *************************************************************)
+(* ITEMS ********************************************************************)
+
+(* atomic items *)
+inductive item0: Type[0] β
+ | Sort: nat β item0 (* sort: starting at 0 *)
+ | LRef: nat β item0 (* reference by index: starting at 0 *)
+.
(* binary binding items *)
inductive bind2: Type[0] β
-| Abbr: bind2 (* abbreviation *)
-| Abst: bind2 (* abstraction *)
+ | Abbr: bind2 (* abbreviation *)
+ | Abst: bind2 (* abstraction *)
.
(* binary non-binding items *)
inductive flat2: Type[0] β
-| Appl: flat2 (* application *)
-| Cast: flat2 (* explicit type annotation *)
+ | Appl: flat2 (* application *)
+ | Cast: flat2 (* explicit type annotation *)
.
(* binary items *)
inductive item2: Type[0] β
-| Bind: bind2 β item2 (* binding item *)
-| Flat: flat2 β item2 (* non-binding item *)
+ | Bind: bind2 β item2 (* binding item *)
+ | Flat: flat2 β item2 (* non-binding item *)
.
coercion item2_of_bind2: βI:bind2.item2 β Bind on _I:bind2 to item2.
(* terms *)
inductive term: Type[0] β
-| TSort: nat β term (* sort: starting at 0 *)
-| TLRef: nat β term (* reference by index: starting at 0 *)
-| TPair: item2 β term β term β term (* binary item construction *)
+ | TAtom: item0 β term (* atomic item construction *)
+ | TPair: item2 β term β term β term (* binary item construction *)
.
-interpretation "sort (term)" 'Star k = (TSort k).
+interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
-interpretation "local reference (term)" 'LRef i = (TLRef i).
+interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
+
+interpretation "term construction (atomic)" 'SItem I = (TAtom I).
interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
(* SIMPLE (NEUTRAL) TERMS ***************************************************)
inductive simple: term β Prop β
- | simple_sort: βk. simple (βk)
- | simple_lref: βi. simple (#i)
+ | simple_atom: βI. simple (π{I})
| simple_flat: βI,V,T. simple (π{I} V. T)
.
fact simple_inv_bind_aux: βT. π[T] β βJ,W,U. T = π{J} W. U β False.
#T * -T
-[ #k #J #W #U #H destruct
-| #k #J #W #U #H destruct
+[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
(* WEIGHT OF A TERM *********************************************************)
let rec tw T β match T with
-[ TSort _ β 1
-| TLRef _ β 1
+[ TAtom _ β 1
| TPair _ V T β tw V + tw T + 1
].
(* HOMOMORPHIC TERMS ********************************************************)
inductive thom: term β term β Prop β
- | thom_sort: βk. thom (βk) (βk)
- | thom_lref: βi. thom (#i) (#i)
- | thom_abst: βV1,V2,T1,T2. thom (π{Abst} V1. T1) (π{Abst} V2. T2)
+ | thom_atom: βI. thom (π{I}) (π{I})
+ | thom_abst: βV1,V2,T1,T2. thom (π{Abst} V1. T1) (π{Abst} V2. T2)
| thom_appl: βV1,V2,T1,T2. thom T1 T2 β π[T1] β π[T2] β
- thom (Γ°\9d\95\9a{Appl} V1. T1) (Γ°\9d\95\9a{Appl} V2. T2)
+ thom (Γ°\9d\95\94{Appl} V1. T1) (Γ°\9d\95\94{Appl} V2. T2)
.
interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
non associative with precedence 90
for @{ 'LRef $k }.
-notation "hvbox( π { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( π { I } )"
+ non associative with precedence 90
+ for @{ 'SItem $I }.
+
+notation "hvbox( π { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
for @{ 'SItem $I $T1 $T }.
notation "hvbox( T . break π { I } break term 90 T1 )"
non associative with precedence 89
for @{ 'DBind $T $I $T1 }.
-
+(*
+notation > "hvbox( T . break π { I } break term 90 T1 )"
+ non associative with precedence 89
+ for @{ 'DBind $T $I $T1 }.
+*) (**) (* this breaks all parsing *)
notation "hvbox( # [ x ] )"
non associative with precedence 90
for @{ 'Weight $x }.
qed.
lemma cpr_cast: βL,V,T1,T2.
- L Γ’\8aΒ’ T1 Γ’\87\92 T2 Γ’\86\92 L Γ’\8aΒ’ Γ°\9d\95\97{Cast} V. T1 β T2.
+ L Γ’\8aΒ’ T1 Γ’\87\92 T2 Γ’\86\92 L Γ’\8aΒ’ Γ°\9d\95\94{Cast} V. T1 β T2.
#L #V #T1 #T2 * /3/
qed.
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
inductive tpr: term β term β Prop β
-| tpr_sort : βk. tpr (βk) (βk)
-| tpr_lref : βi. tpr (#i) (#i)
+| tpr_atom : βI. tpr (π{I}) (π{I})
| tpr_flat : βI,V1,V2,T1,T2. tpr V1 V2 β tpr T1 T2 β
tpr (π{I} V1. T1) (π{I} V2. T2)
| tpr_beta : βV1,V2,W,T1,T2.
tpr V1 V2 β tpr T1 T2 β
- tpr (Γ°\9d\95\9a{Appl} V1. Γ°\9d\95\9a{Abst} W. T1) (Γ°\9d\95\9a{Abbr} V2. T2)
+ tpr (Γ°\9d\95\94{Appl} V1. Γ°\9d\95\94{Abst} W. T1) (Γ°\9d\95\94{Abbr} V2. T2)
| tpr_delta: βI,V1,V2,T1,T2,T.
tpr V1 V2 β tpr T1 T2 β β. π{I} V2 β’ T2 [0, 1] β« T β
- tpr (Γ°\9d\95\9a{I} V1. T1) (Γ°\9d\95\9a{I} V2. T)
+ tpr (Γ°\9d\95\93{I} V1. T1) (Γ°\9d\95\93{I} V2. T)
| tpr_theta: βV,V1,V2,W1,W2,T1,T2.
tpr V1 V2 β β[0,1] V2 β‘ V β tpr W1 W2 β tpr T1 T2 β
- tpr (Γ°\9d\95\9a{Appl} V1. Γ°\9d\95\9a{Abbr} W1. T1) (Γ°\9d\95\9a{Abbr} W2. Γ°\9d\95\9a{Appl} V. T2)
+ tpr (Γ°\9d\95\94{Appl} V1. Γ°\9d\95\94{Abbr} W1. T1) (Γ°\9d\95\94{Abbr} W2. Γ°\9d\95\94{Appl} V. T2)
| tpr_zeta : βV,T,T1,T2. β[0,1] T1 β‘ T β tpr T1 T2 β
- tpr (Γ°\9d\95\9a{Abbr} V. T) T2
-| tpr_tau : Γ’\88\80V,T1,T2. tpr T1 T2 Γ’\86\92 tpr (Γ°\9d\95\9a{Cast} V. T1) T2
+ tpr (Γ°\9d\95\94{Abbr} V. T) T2
+| tpr_tau : Γ’\88\80V,T1,T2. tpr T1 T2 Γ’\86\92 tpr (Γ°\9d\95\94{Cast} V. T1) T2
.
interpretation
(* Basic properties *********************************************************)
lemma tpr_bind: βI,V1,V2,T1,T2. V1 β V2 β T1 β T2 β
- π{I} V1. T1 β π{I} V2. T2.
+ π{I} V1. T1 β π{I} V2. T2.
/2/ qed.
lemma tpr_refl: βT. T β T.
(* Basic inversion lemmas ***************************************************)
-fact tpr_inv_sort1_aux: βU1,U2. U1 β U2 β βk. U1 = βk β U2 = βk.
+fact tpr_inv_atom1_aux: βU1,U2. U1 β U2 β βI. U1 = π{I} β U2 = π{I}.
#U1 #U2 * -U1 U2
-[ #k0 #k #H destruct -k0 //
-| #i #k #H destruct
+[ //
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
]
qed.
-lemma tpr_inv_sort1: βk,U2. βk β U2 β U2 = βk.
-/2/ qed.
-
-fact tpr_inv_lref1_aux: βU1,U2. U1 β U2 β βi. U1 = #i β U2 = #i.
-#U1 #U2 * -U1 U2
-[ #k #i #H destruct
-| #j #i #H destruct -j //
-| #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 #_ #_ #i #H destruct
-| #V #T1 #T2 #_ #i #H destruct
-]
-qed.
-
-lemma tpr_inv_lref1: βi,U2. #i β U2 β U2 = #i.
+lemma tpr_inv_atom1: βI,U2. π{I} β U2 β U2 = π{I}.
/2/ qed.
fact tpr_inv_bind1_aux: βU1,U2. U1 β U2 β βI,V1,T1. U1 = π{I} V1. T1 β
(ββV2,T2,T. V1 β V2 & T1 β T2 &
β. π{I} V2 β’ T2 [0, 1] β« T &
- U2 = Γ°\9d\95\9a{I} V2. T
+ U2 = Γ°\9d\95\93{I} V2. T
) β¨
ββT. β[0,1] T β‘ T1 & T β U2 & I = Abbr.
#U1 #U2 * -U1 U2
-[ #k #I #V #T #H destruct
-| #i #I #V #T #H destruct
+[ #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/
lemma tpr_inv_bind1: βV1,T1,U2,I. π{I} V1. T1 β U2 β
(ββV2,T2,T. V1 β V2 & T1 β T2 &
β. π{I} V2 β’ T2 [0, 1] β« T &
- U2 = Γ°\9d\95\9a{I} V2. T
+ U2 = Γ°\9d\95\93{I} V2. T
) β¨
ββT. β[0,1] T β‘ T1 & tpr T U2 & I = Abbr.
/2/ qed.
-lemma tpr_inv_abbr1: Γ’\88\80V1,T1,U2. Γ°\9d\95\9a{Abbr} V1. T1 β U2 β
+lemma tpr_inv_abbr1: Γ’\88\80V1,T1,U2. Γ°\9d\95\93{Abbr} V1. T1 β U2 β
(ββV2,T2,T. V1 β V2 & T1 β T2 &
β. π{Abbr} V2 β’ T2 [0, 1] β« T &
- U2 = Γ°\9d\95\9a{Abbr} V2. T
+ U2 = Γ°\9d\95\93{Abbr} V2. T
) β¨
ββT. β[0,1] T β‘ T1 & tpr T U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 β¦ H) -H * /3 width=7/
qed.
-fact tpr_inv_appl1_aux: βU1,U2. U1 β U2 β βV1,U0. U1 = π{Appl} V1. U0 β
+fact tpr_inv_flat1_aux: βU1,U2. U1 β U2 β βI,V1,U0. U1 = π{I} V1. U0 β
β¨β¨ ββV2,T2. V1 β V2 & U0 β T2 &
- U2 = Γ°\9d\95\9a{Appl} V2. T2
+ U2 = Γ°\9d\95\97{I} V2. T2
| ββV2,W,T1,T2. V1 β V2 & T1 β T2 &
- U0 = Γ°\9d\95\9a{Abst} W. T1 &
- U2 = Γ°\9d\95\93{Abbr} V2. T2
+ U0 = Γ°\9d\95\94{Abst} W. T1 &
+ U2 = Γ°\9d\95\94{Abbr} V2. T2 & I = Appl
| ββV2,V,W1,W2,T1,T2. V1 β V2 & W1 β W2 & T1 β T2 &
β[0,1] V2 β‘ V &
- U0 = π{Abbr} W1. T1 &
- U2 = π{Abbr} W2. π{Appl} V. T2.
+ U0 = π{Abbr} W1. T1 &
+ U2 = π{Abbr} W2. π{Appl} V. T2 &
+ I = Appl
+ | (U0 β U2 β§ I = Cast).
#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
- destruct -V1 T0 /3 width=12/
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
+[ #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 #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 #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
]
qed.
-lemma tpr_inv_appl1: βV1,U0,U2. π{Appl} V1. U0 β U2 β
+lemma tpr_inv_flat1: βV1,U0,U2,I. π{I} V1. U0 β U2 β
β¨β¨ ββV2,T2. V1 β V2 & U0 β T2 &
- U2 = Γ°\9d\95\9a{Appl} V2. T2
+ U2 = Γ°\9d\95\97{I} V2. T2
| ββV2,W,T1,T2. V1 β V2 & T1 β T2 &
- U0 = Γ°\9d\95\9a{Abst} W. T1 &
- U2 = Γ°\9d\95\93{Abbr} V2. T2
+ U0 = Γ°\9d\95\94{Abst} W. T1 &
+ U2 = Γ°\9d\95\94{Abbr} V2. T2 & I = Appl
| ββV2,V,W1,W2,T1,T2. V1 β V2 & W1 β W2 & T1 β T2 &
β[0,1] V2 β‘ V &
- U0 = π{Abbr} W1. T1 &
- U2 = π{Abbr} W2. π{Appl} V. T2.
-/2/ qed.
-
-fact tpr_inv_cast1_aux: βU1,U2. U1 β U2 β βV1,T1. U1 = π{Cast} V1. T1 β
- (ββV2,T2. V1 β V2 & T1 β T2 & U2 = π{Cast} V2. T2)
- β¨ T1 β U2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
-]
-qed.
-
-lemma tpr_inv_cast1: βV1,T1,U2. π{Cast} V1. T1 β U2 β
- (ββV2,T2. V1 β V2 & T1 β T2 & U2 = π{Cast} V2. T2)
- β¨ T1 β U2.
+ U0 = π{Abbr} W1. T1 &
+ U2 = π{Abbr} W2. π{Appl} V. T2 &
+ I = Appl
+ | (U0 β U2 β§ I = Cast).
/2/ qed.
-lemma tpr_inv_flat1: βV1,U0,U2,I. π{I} V1. U0 β U2 β
+lemma tpr_inv_appl1: βV1,U0,U2. π{Appl} V1. U0 β U2 β
β¨β¨ ββV2,T2. V1 β V2 & U0 β T2 &
- U2 = Γ°\9d\95\97{I} V2. T2
+ U2 = Γ°\9d\95\94{Appl} V2. T2
| ββV2,W,T1,T2. V1 β V2 & T1 β T2 &
- U0 = Γ°\9d\95\9a{Abst} W. T1 &
- U2 = Γ°\9d\95\93{Abbr} V2. T2 & I = Appl
+ U0 = Γ°\9d\95\94{Abst} W. T1 &
+ U2 = Γ°\9d\95\94{Abbr} V2. T2
| ββV2,V,W1,W2,T1,T2. V1 β V2 & W1 β W2 & T1 β T2 &
β[0,1] V2 β‘ V &
- U0 = π{Abbr} W1. T1 &
- U2 = π{Abbr} W2. π{Appl} V. T2 &
- I = Appl
- | (U0 β U2 β§ I = Cast).
-#V1 #U0 #U2 * #H
-[ elim (tpr_inv_appl1 β¦ H) -H * /3 width=12/
-| elim (tpr_inv_cast1 β¦ H) -H [1: *] /3 width=5/
+ U0 = π{Abbr} W1. T1 &
+ U2 = π{Abbr} W2. π{Appl} V. T2.
+#V1 #U0 #U2 #H
+elim (tpr_inv_flat1 β¦ H) -H * /3 width=12/ #_ #H destruct
+qed.
+
+lemma tpr_inv_cast1: βV1,T1,U2. π{Cast} V1. T1 β U2 β
+ (ββV2,T2. V1 β V2 & T1 β T2 & U2 = π{Cast} V2. T2)
+ β¨ T1 β U2.
+#V1 #T1 #U2 #H
+elim (tpr_inv_flat1 β¦ H) -H * /3 width=5/
+[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
+| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
]
qed.
fact tpr_inv_lref2_aux: βT1,T2. T1 β T2 β βi. T2 = #i β
β¨β¨ T1 = #i
| ββV,T,T0. β[O,1] T0 β‘ T & T0 β #i &
- T1 = Γ°\9d\95\9a{Abbr} V. T
- | Γ’\88\83Γ’\88\83V,T. T Γ’\87\92 #i & T1 = Γ°\9d\95\9a{Cast} V. T.
+ T1 = Γ°\9d\95\94{Abbr} V. T
+ | Γ’\88\83Γ’\88\83V,T. T Γ’\87\92 #i & T1 = Γ°\9d\95\94{Cast} V. T.
#T1 #T2 * -T1 T2
-[ #k #i #H destruct
-| #j #i /2/
+[ #I #i #H destruct /2/
| #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
lemma tpr_inv_lref2: βT1,i. T1 β #i β
β¨β¨ T1 = #i
| ββV,T,T0. β[O,1] T0 β‘ T & T0 β #i &
- T1 = Γ°\9d\95\93{Abbr} V. T
- | Γ’\88\83Γ’\88\83V,T. T Γ’\87\92 #i & T1 = Γ°\9d\95\97{Cast} V. T.
+ T1 = Γ°\9d\95\94{Abbr} V. T
+ | Γ’\88\83Γ’\88\83V,T. T Γ’\87\92 #i & T1 = Γ°\9d\95\94{Cast} V. T.
/2/ qed.
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
-[ #k #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono β¦ HU1 β¦ HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_sort1 β¦ HU2) -HU2 #H destruct -U2 //
-| #i #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono β¦ HU1 β¦ HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_lref1 β¦ HU2) * * #Hid #H destruct -U2 //
+[ * #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 //
+ ]
| #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/
βd,e,U1. β[d, e] U1 β‘ T1 β
ββU2. β[d, e] U2 β‘ T2 & U1 β U2.
#T1 #T2 #H elim H -H T1 T2
-[ #k #d #e #U1 #HU1
- lapply (lift_inv_sort2 β¦ HU1) -HU1 #H destruct -U1 /2/
-| #i #d #e #U1 #HU1
- lapply (lift_inv_lref2 β¦ HU1) -HU1 * * #Hid #H destruct -U1 /3/
+[ * #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/
+ ]
| #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;
(* Advanced inversion lemmas ************************************************)
-fact tpr_inv_abst1_aux: Γ’\88\80U1,U2. U1 Γ’\87\92 U2 Γ’\86\92 Γ’\88\80V1,T1. U1 = Γ°\9d\95\9a{Abst} V1. T1 β
- Γ’\88\83Γ’\88\83V2,T2. V1 Γ’\87\92 V2 & T1 Γ’\87\92 T2 & U2 = Γ°\9d\95\9a{Abst} V2. T2.
+fact tpr_inv_abst1_aux: Γ’\88\80U1,U2. U1 Γ’\87\92 U2 Γ’\86\92 Γ’\88\80V1,T1. U1 = Γ°\9d\95\94{Abst} V1. T1 β
+ Γ’\88\83Γ’\88\83V2,T2. V1 Γ’\87\92 V2 & T1 Γ’\87\92 T2 & U2 = Γ°\9d\95\94{Abst} V2. T2.
#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
+[ #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;
]
qed.
-lemma tpr_inv_abst1: Γ’\88\80V1,T1,U2. Γ°\9d\95\9a{Abst} V1. T1 β U2 β
- Γ’\88\83Γ’\88\83V2,T2. V1 Γ’\87\92 V2 & T1 Γ’\87\92 T2 & U2 = Γ°\9d\95\9a{Abst} V2. T2.
+lemma tpr_inv_abst1: Γ’\88\80V1,T1,U2. Γ°\9d\95\94{Abst} V1. T1 β U2 β
+ Γ’\88\83Γ’\88\83V2,T2. V1 Γ’\87\92 V2 & T1 Γ’\87\92 T2 & U2 = Γ°\9d\95\94{Abst} V2. T2.
/2/ qed.
(* Confluence lemmas ********************************************************)
-fact tpr_conf_sort_sort: βk. ββX. βk β X & βk β X.
-/2/ qed.
-
-fact tpr_conf_lref_lref: βi. ββX. #i β X & #i β X.
+fact tpr_conf_atom_atom: βI. ββX. π{I} β X & π{I} β X.
/2/ qed.
fact tpr_conf_flat_flat:
ββX. X1 β X & X2 β X
) β
V0 β V1 β V0 β V2 β
- U0 Γ’\87\92 T2 Γ’\86\92 Γ°\9d\95\93{Abst} W0. U0 β T1 β
- Γ’\88\83Γ’\88\83X. Γ°\9d\95\97{Appl} V1. T1 Γ’\87\92 X & Γ°\9d\95\93{Abbr} V2. T2 β X.
+ U0 Γ’\87\92 T2 Γ’\86\92 Γ°\9d\95\94{Abst} W0. U0 β T1 β
+ Γ’\88\83Γ’\88\83X. Γ°\9d\95\94{Appl} V1. T1 Γ’\87\92 X & Γ°\9d\95\94{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
ββX. X1 β X & X2 β X
) β
V0 β V1 β V0 β V2 β β[O,1] V2 β‘ V β
- W0 Γ’\87\92 W2 Γ’\86\92 U0 Γ’\87\92 U2 Γ’\86\92 Γ°\9d\95\93{Abbr} W0. U0 β T1 β
- Γ’\88\83Γ’\88\83X. Γ°\9d\95\97{Appl} V1. T1 Γ’\87\92 X & Γ°\9d\95\93{Abbr} W2. Γ°\9d\95\97{Appl} V. U2 β X.
+ W0 Γ’\87\92 W2 Γ’\86\92 U0 Γ’\87\92 U2 Γ’\86\92 Γ°\9d\95\94{Abbr} W0. U0 β T1 β
+ Γ’\88\83Γ’\88\83X. Γ°\9d\95\94{Appl} V1. T1 Γ’\87\92 X & Γ°\9d\95\94{Abbr} W2. Γ°\9d\95\94{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 (lift_total VV 0 1) #VVV #HVV
ββX. X1 β X & X2 β X
) β
V0 β V1 β T0 β T1 β T0 β X2 β
- Γ’\88\83Γ’\88\83X. Γ°\9d\95\97{Cast} V1. T1 β X & X2 β X.
+ Γ’\88\83Γ’\88\83X. Γ°\9d\95\94{Cast} V1. T1 β X & X2 β X.
#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
elim (IH β¦ HT01 β¦ HT02) -HT01 HT02 IH /3/
qed.
ββX. X1 β X & X2 β X
) β
V0 β V1 β V0 β V2 β T0 β T1 β T0 β T2 β
- Γ’\88\83Γ’\88\83X. Γ°\9d\95\93{Abbr} V1. T1 Γ’\87\92X & Γ°\9d\95\93{Abbr} V2. T2 β X.
+ Γ’\88\83Γ’\88\83X. Γ°\9d\95\94{Abbr} V1. T1 Γ’\87\92X & Γ°\9d\95\94{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/
) β
V0 β V1 β V0 β V2 β W0 β W1 β W0 β W2 β T0 β T1 β T0 β T2 β
β[O, 1] V1 β‘ VV1 β β[O, 1] V2 β‘ VV2 β
- Γ’\88\83Γ’\88\83X. Γ°\9d\95\93{Abbr} W1. Γ°\9d\95\97{Appl} VV1. T1 Γ’\87\92 X & Γ°\9d\95\93{Abbr} W2. Γ°\9d\95\97{Appl} VV2. T2 β X.
+ Γ’\88\83Γ’\88\83X. Γ°\9d\95\94{Abbr} W1. Γ°\9d\95\94{Appl} VV1. T1 Γ’\87\92 X & Γ°\9d\95\94{Abbr} W2. Γ°\9d\95\94{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
βX0,X1,X2. X0 β X1 β X0 β X2 β X0 = Y0 β
ββX. X1 β X & X2 β X.
#Y0 #IH #X0 #X1 #X2 * -X0 X1
-[ #k1 #H1 #H2 destruct -Y0;
- lapply (tpr_inv_sort1 β¦ H1) -H1
-(* case 1: sort, sort *)
- #H1 destruct -X2 //
-| #i1 #H1 #H2 destruct -Y0;
- lapply (tpr_inv_lref1 β¦ H1) -H1
-(* case 2: lref, lref *)
+[ #I1 #H1 #H2 destruct -Y0;
+ lapply (tpr_inv_atom1 β¦ H1) -H1
+(* case 1: atom, atom *)
#H1 destruct -X2 //
| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
elim (tpr_inv_flat1 β¦ H1) -H1 *
-(* case 3: flat, flat *)
+(* case 2: flat, flat *)
[ #V2 #T2 #HV02 #HT02 #H destruct -X2
/3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
-(* case 4: flat, beta *)
+(* case 3: flat, beta *)
| #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
/3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 5: flat, theta *)
+(* case 4: flat, theta *)
| #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
/3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
-(* case 6: flat, tau *)
+(* case 5: flat, tau *)
| #HT02 #H destruct -I
/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;
elim (tpr_inv_appl1 β¦ H1) -H1 *
-(* case 7: beta, flat (repeated) *)
+(* case 6: beta, flat (repeated) *)
[ #V2 #T2 #HV02 #HT02 #H destruct -X2
@ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
-(* case 8: beta, beta *)
+(* case 7: beta, beta *)
| #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
/3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 9, beta, theta (excluded) *)
+(* 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;
elim (tpr_inv_bind1 β¦ H1) -H1 *
-(* case 10: delta, delta *)
+(* case 9: delta, delta *)
[ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
/3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 11: delta, zata *)
+(* case 10: delta, zata *)
| #T2 #HT20 #HTX2 #H destruct -I1;
/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;
elim (tpr_inv_appl1 β¦ H1) -H1 *
-(* case 12: theta, flat (repeated) *)
+(* case 11: theta, flat (repeated) *)
[ #V2 #T2 #HV02 #HT02 #H destruct -X2
@ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
-(* case 13: theta, beta (repeated) *)
+(* case 12: theta, beta (repeated) *)
| #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
-(* case 14: theta, theta *)
+(* case 13: theta, theta *)
| #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
/3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
]
| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
elim (tpr_inv_abbr1 β¦ H1) -H1 *
-(* case 15: zeta, delta (repeated) *)
+(* case 14: zeta, delta (repeated) *)
[ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
@ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
-(* case 16: zeta, 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;
elim (tpr_inv_cast1 β¦ H1) -H1
-(* case 17: tau, flat (repeated) *)
+(* case 16: tau, flat (repeated) *)
[ * #V2 #T2 #HV02 #HT02 #H destruct -X2
@ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
-(* case 18: tau, tau *)
+(* case 17: tau, tau *)
| #HT02
/2 by tpr_conf_tau_tau/
]
(* Basic-1: removed theorems 18:
drop_skip_flat
- cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
+ cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
drop_clear drop_clear_O drop_clear_S
clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
clear_gen_all clear_clear clear_mono clear_trans clear_ctail
lemma lift_refl: βT,d. β[d, 0] T β‘ T.
#T elim T -T
-[ //
-| #i #d elim (lt_or_ge i d) /2/
-| #I elim I -I /2/
+[ * #i // #d elim (lt_or_ge i d) /2/
+| * /2/
]
qed.
lemma lift_total: βT1,d,e. βT2. β[d,e] T1 β‘ T2.
#T1 elim T1 -T1
-[ /2/
-| #i #d #e elim (lt_or_ge i d) /3/
+[ * #i /2/ #d #e elim (lt_or_ge i d) /3/
| * #I #V1 #T1 #IHV1 #IHT1 #d #e
elim (IHV1 d e) -IHV1 #V2 #HV12
[ elim (IHT1 (d+1) e) -IHT1 /3/
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
inductive tps: lenv β term β nat β nat β term β Prop β
-| tps_sort : βL,k,d,e. tps L (βk) d e (βk)
-| tps_lref : βL,i,d,e. tps L (#i) d e (#i)
+| tps_atom : βL,I,d,e. tps L (π{I}) d e (π{I})
| tps_subst: βL,K,V,W,i,d,e. d β€ i β i < d + e β
β[0, i] L β‘ K. π{Abbr} V β β[0, i + 1] V β‘ W β tps L (#i) d e W
| tps_bind : βL,I,V1,V2,T1,T2,d,e.
βL2. L1 [d, e] β L2 β L2 β’ T1 [d, e] β« T2.
#L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e
[ //
-| //
| #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
elim (drop_leq_drop1 β¦ HL12 β¦ HLK1 ? ?) -HL12 HLK1 // /2/
| /4/
L β’ T1 [d2, e2] β« T2.
#L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1
[ //
-| //
| #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
lapply (transitive_le β¦ Hd12 β¦ Hid1) -Hd12 Hid1 #Hid2
lapply (lt_to_le_to_lt β¦ Hide1 β¦ Hde12) -Hide1 /2/
L β’ T1 [d, e] β« T2 β L β’ T1 [d, |L| - d] β« T2.
#L #T1 #T #d #e #H elim H -L T1 T d e
[ //
-| //
| #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
lapply (drop_fwd_drop2_length β¦ HLK) #Hi
lapply (le_to_lt_to_lt β¦ Hdi Hi) #Hd
ββT. L β’ T1 [d, i - d] β« T & L β’ T [i, d + e - i] β« T2.
#L #T1 #T2 #d #e #H elim H -L T1 T2 d e
[ /2/
-| /2/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
elim (lt_or_ge i j)
[ -Hide Hjde;
β[O, i] L β‘ K. π{Abbr} V &
β[O, i + 1] V β‘ T2.
#L #T1 #T2 #d #e * -L T1 T2 d e
-[ #L #k #d #e #i #H destruct
-| /2/
+[ #L #I #d #e #i #H destruct -I /2/
| #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #j #H destruct -i /3/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
U2 = π{I} V2. T2.
#d #e #L #U1 #U2 * -d e L U1 U2
[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
U2 = π{I} V2. T2.
#d #e #L #U1 #U2 * -d e L U1 U2
[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
fact tps_inv_refl0_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β e = 0 β T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
-| //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e;
lapply (le_to_lt_to_lt β¦ Hdi β¦ Hide) -Hdi Hide <plus_n_O #Hdd
elim (lt_refl_false β¦ Hdd)
dt + et β€ d β
L β’ U1 [dt, et] β« U2.
#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et
-[ #K #k #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
- >(lift_mono β¦ H1 β¦ H2) -H1 H2 //
-| #K #i #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
>(lift_mono β¦ H1 β¦ H2) -H1 H2 //
| #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HVU2 #Hdetd
lapply (lt_to_le_to_lt β¦ Hidet β¦ Hdetd) -Hdetd #Hid
d β€ dt β
L β’ U1 [dt + e, et] β« U2.
#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et
-[ #K #k #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
- >(lift_mono β¦ H1 β¦ H2) -H1 H2 //
-| #K #i #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
>(lift_mono β¦ H1 β¦ H2) -H1 H2 //
| #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt
lapply (transitive_le β¦ Hddt β¦ Hdti) -Hddt #Hid
dt + et β€ d β
ββT2. K β’ T1 [dt, et] β« T2 & β[d, e] T2 β‘ U2.
#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et
-[ #L #k #dt #et #K #d #e #_ #T1 #H #_
- lapply (lift_inv_sort2 β¦ H) -H #H destruct -T1 /2/
-| #L #i #dt #et #K #d #e #_ #T1 #H #_
- elim (lift_inv_lref2 β¦ H) -H * #Hid #H destruct -T1 /3/
+[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
+ [ lapply (lift_inv_sort2 β¦ H) -H #H destruct -T1 /2/
+ | elim (lift_inv_lref2 β¦ H) -H * #Hid #H destruct -T1 /3/
+ ]
| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd
lapply (lt_to_le_to_lt β¦ Hidet β¦ Hdetd) -Hdetd #Hid
lapply (lift_inv_lref2_lt β¦ H β¦ Hid) -H #H destruct -T1;
d + e β€ dt β
ββT2. K β’ T1 [dt - e, et] β« T2 & β[d, e] T2 β‘ U2.
#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et
-[ #L #k #dt #et #K #d #e #_ #T1 #H #_
- lapply (lift_inv_sort2 β¦ H) -H #H destruct -T1 /2/
-| #L #i #dt #et #K #d #e #_ #T1 #H #_
- elim (lift_inv_lref2 β¦ H) -H * #Hid #H destruct -T1 /3/
+[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
+ [ lapply (lift_inv_sort2 β¦ H) -H #H destruct -T1 /2/
+ | elim (lift_inv_lref2 β¦ H) -H * #Hid #H destruct -T1 /3/
+ ]
| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
lapply (transitive_le β¦ Hdedt β¦ Hdti) #Hdei
lapply (plus_le_weak β¦ Hdedt) -Hdedt #Hedt
L β’ U1 [d, e] β« U2 β βT1. β[d, e] T1 β‘ U1 β U1 = U2.
#L #U1 #U2 #d #e #H elim H -H L U1 U2 d e
[ //
-| //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H
elim (lift_inv_lref2 β¦ H) -H * #H
[ lapply (le_to_lt_to_lt β¦ Hdi β¦ H) -Hdi H #H
βK,V. β[0, d] L β‘ K. π{Abst} V β T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
-| //
| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
>(le_to_le_to_eq β¦ Hdi ?) /2/ -d #K #V #HLK
lapply (drop_mono β¦ HLK0 β¦ HLK) #H destruct
ββT. L β’ T1 [d, e] β« T & L β’ T2 [d, e] β« T.
#L #T0 #T1 #d #e #H elim H -H L T0 T1 d e
[ /2/
-| /2/
| #L #K1 #V1 #T1 #i1 #d #e #Hdi1 #Hi1de #HLK1 #HVT1 #T2 #H
elim (tps_inv_lref1 β¦ H) -H
[ #HX destruct -T2 /4/
ββT. L β’ T1 [d2, e2] β« T & L β’ T [d1, e1] β« T2.
#L #T1 #T0 #d1 #e1 #H elim H -L T1 T0 d1 e1
[ /2/
-| /2/
| #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
lapply (transitive_le β¦ Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak β¦ HWT2 0 (i1 + 1) ? ?) -HWT2; normalize /2/ -Hde2i1 #HWT2
projects / helm.git / commitdiff