lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
#s elim s -s //
-#p #s #IHs * /3 width=1/
+#p #s #IHs * /3 width=1/
qed.
lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
-#r elim r -r //
-#q #r #IHr * /3 width=1/
+/2 width=1 by All_append/
qed.
+lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s.
+/2 width=1 by All_inv_append/
+qed-.
+
definition ho_compatible_rc: predicate (trace→relation term) ≝ λR.
∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
-#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+#R #HR #s #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
qed.
lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
-#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l … s B1 H) -s -B1 // /3 width=3/
qed.
lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
-#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
qed.