| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#b0 #T0 #HT02 #H destruct
lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/
]
| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_sn … HF1 … Hp) -HF1 -p #b1 #V1 #V #T1 #HV1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#b0 #V0 #T0 #HV02 #H destruct
lapply (pl_sts_step_sn … HV1 … HV02) -V /2 width=5/
]
| #p #s #F1 #F #HF1 #_ #IHF2 #r #H
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_dx … HF1 … Hp) -HF1 -p #b0 #V0 #T1 #T #HT1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#T0 #HT02 #H destruct
lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=3/
]
∃∃b1,V1,T1,T0. V1 Ⓡ↦*[r] V2 & T1 Ⓡ↦*[s] T0 & {b1}@V1.T1 = F1.
#b2 #s #r #F1 #V2 #T2 #H
elim (pl_sts_inv_trans … H) -H #F #HF1 #H
-elim (pl_sts_inv_sn_appl_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+elim (pl_sts_inv_sn_appl_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#b #V #T #HV2 #H destruct
-elim (pl_sts_inv_dx_appl_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+elim (pl_sts_inv_dx_appl_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#T1 #HT1 #H destruct /2 width=7/
qed-.
theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
#s elim s -s // #p1 * //
#p2 #s #IHs #F1 #F2 #H
-elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
-elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
+elim (pl_sts_inv_cons … H …) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
+elim (pl_sts_inv_cons … H …) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
qed-.
[ #_ @(ex2_2_intro … ◊ ◊) // (**) (* auto needs some help here *)
| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
lapply (is_standard_fwd_cons … Hs) #H
- elim (IHF1 ?) // -IHF1 -H #r1 #r2 #Hr1 #H destruct
+ elim (IHF1 …) // -IHF1 -H #r1 #r2 #Hr1 #H destruct
elim (in_whd_or_in_inner p) #Hp
[ -Hs -F1 -F -T2 -b2
@(ex2_2_intro … (p::r1) r2) // /2 width=1/ (**) (* auto needs some help here *)
elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp
(* case 1: dx *)
[ -IHq
- elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
#b #T #_ #HT -T2
- elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_st_inv_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#c #V #T1 #T0 #_ #_ #HT0 -q -T1 -F1 destruct
(* case 2: rc *)
| destruct -F1 -F -T2 -b2
@(ex2_2_intro … ◊ (q::r2)) // (**) (* auto needs some help here *)
(* case 3: sn *)
- | elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ | elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
#b #T #_ #HT -T2
- elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_st_inv_sn … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#c #V1 #V #T0 #_ #_ #HT0 -c -q -V1 -F1 destruct
]
]
[ #_ @(ex3_3_intro … ◊ ◊ ◊) // (**) (* auto needs some help here *)
| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
lapply (is_standard_fwd_cons … Hs) #H
- elim (IHF1 ?) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
+ elim (IHF1 …) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
elim (in_whd_or_in_inner p) #Hp
[ -Hs -F1 -F -V2 -T2 -b2
@(ex3_3_intro … (p::r1) r2 r3) // /2 width=1/ (**) (* auto needs some help here *)
elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
elim (pl_sts_fwd_abst_dx … HM1) #r1 #r2 #Hr1 #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
<(map_cons_append … r2 (p::◊)) #H
lapply (is_standard_inv_compatible_rc … H) -H #Hp
- elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
+ elim (pl_sts_inv_rc_abst_dx … HT …) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct
- elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
+ elim (IHA12 … HT02 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
@(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| #p #B1 #B2 #A #_ #IHB12 #F #HF #s #M1 #HM1 #Hs
elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #_ #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
>associative_append #Hs
lapply (is_standard_inv_compatible_sn … H) -H #Hp
elim (pl_sts_fwd_dx_sn_appl_dx … HT) -HT #b0 #V0 #T0 #T1 #HV0 #_ #H -T1 -r2
elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #H #_ #_ -b0 -M0 -T0 destruct
- elim (IHB12 … HV0 ?) // -r3 -B0 -IHB12 #G2 #HG2 #H
+ elim (IHB12 … HV0 …) // -r3 -B0 -IHB12 #G2 #HG2 #H
@(ex2_intro … ({⊥}@G2.{⊥}⇕T)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| #p #B #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
>associative_append #Hs
lapply (is_whd_is_inner_inv … Hr2) -Hr2 // -H #H destruct
lapply (pl_sts_inv_nil … HT ?) -HT // #H
elim (boolean_inv_appl … H) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
- elim (IHA12 … A0 ??) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *)
+ elim (IHA12 … A0 …) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *)
#F2 #HF2 #H
@(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| <(map_cons_append … r2 (p::◊)) in Hs; #H
lapply (is_standard_inv_compatible_dx … H ?) -H /3 width=1/ -Hp #Hp
>append_nil in HT; #HT
- elim (pl_sts_inv_dx_appl_dx … HT ??) -HT [3: // |2: skip ] (* simplify line *)
+ elim (pl_sts_inv_dx_appl_dx … HT …) -HT [3: // |2: skip ] (* simplify line *)
#T0 #HT0 #H
elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
- elim (IHA12 … HT0 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
+ elim (IHA12 … HT0 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
@(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
]
| -IHA12 -Hr2 -M0 * #q #r #H destruct
lapply (is_standard_fwd_append_dx … Hs) -r2 #Hs
lapply (is_standard_fwd_sle … Hs) -r #H
- elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#q0 #_ #H destruct
]
]
#p #s #M #M2 #_ #HM2 #IHM1 #Hsp
lapply (is_standard_fwd_append_sn … Hsp) #Hs
elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
-elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
+elim (pl_sred_is_standard_pl_st … HM2 … HM1 …) -HM2 // -M -Hsp #F2 #HF2 #HFM2
lapply (pl_sts_step_dx … HM1 … HF2) -F
#H @(ex2_intro … F2) // (**) (* auto needs some help here *)
qed-.