+lemma pl_sts_fwd_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
+ (∃r2. rc:::r2 = s) ∨ ∃∃r1,r2. r1@◊::rc:::r2 = s.
+#b2 #s #F1 #T2 #H
+lapply (pl_sts_fwd_is_standard … H)
+@(lstar_ind_l … s F1 H) -s -F1
+[ #_ @or_introl @(ex_intro … ◊) // (**) (* auto needs some help here *)
+| * [ | * #p ] #s #F1 #F #HF1 #HF #IHF #Hs
+ lapply (is_standard_fwd_cons … Hs) #H
+ elim (IHF H) -IHF -H * [2,4,6,8: #r1 ] #r2 #H destruct
+(* case 1: ◊, @ *)
+ [ -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … (◊::r1) r2) // (**) (* auto needs some help here *)
+(* case 2: rc, @ *)
+ | -F1 -F -T2 -b2
+ lapply (is_standard_fwd_sle … Hs) -Hs #H
+ lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
+(* case 3: sn, @ *)
+ | -F1 -F -T2 -b2
+ lapply (is_standard_fwd_sle … Hs) -Hs #H
+ lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
+(* case 4: dx, @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … ((dx::p)::r1) r2) // (**) (* auto needs some help here *)
+(* case 5: ◊, no @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … ◊ r2) // (**) (* auto needs some help here *)
+(* case 6, rc, no @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_introl @(ex_intro … (p::r2)) // (**) (* auto needs some help here *)
+(* case 7: sn, no @ *)
+ | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ #b #T #_ #HT -Hs -T2
+ elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ #c #V1 #V #T0 #_ #_ #HT0 -c -V1 -F1 destruct
+(* case 8: dx, no @ *)
+ | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ #b #T #_ #HT -Hs -T2
+ elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ #c #V #T1 #T0 #_ #_ #HT0 -T1 -F1 destruct
+ ]
+]
+qed-.
+
+lemma pl_sts_fwd_abst_dx_is_whd: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
+ ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s.
+#b2 #s #F1 #T2 #H
+lapply (pl_sts_fwd_is_standard … H)
+elim (pl_sts_fwd_abst_dx … H) -b2 -F1 -T2 * [ | #r1 ] #r2 #Hs destruct
+[ #_ @(ex2_2_intro … ◊ r2) //
+| <(associative_append … r1 (◊::◊) (rc:::r2)) #Hs
+ lapply (is_standard_fwd_append_sn … Hs) -Hs #H
+ lapply (is_standard_fwd_is_whd … H) -H // /4 width=4/
+]
+qed-.
+