-lemma lhap1_inv_abst_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀A. 𝛌.A = M → ⊥.
-#p #M #N * -p -M -N
-[ #B #A #A0 #H destruct
-| #p #B #A1 #A2 #_ #A0 #H destruct
-]
-qed-.
-
-lemma lhap1_inv_appl_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀B,A. @B.A = M →
- (∃∃C. ◊ = p & 𝛌.C = A & [⬐B]C = N) ∨
- ∃∃q,C. A ⓗ⇀[q] C & dx::q = p & @B.C = N.
-#p #M #N * -p -M -N
-[ #B #A #B0 #A0 #H destruct /3 width=3/
-| #p #B #A1 #A2 #HA12 #B0 #A0 #H destruct /3 width=5/
-]
-qed-.
-
-lemma lhap1_inv_abst_dx: ∀p,M,N. M ⓗ⇀[p] N → ∀C. 𝛌.C = N →
- ∃∃B,A. ◊ = p & @B.𝛌.A = M & 𝛌.C = [⬐B]A.
-#p #M #N * -p -M -N
-[ #B #A #C #H /2 width=4/
-| #p #B #A1 #A2 #_ #C #H destruct
-]
-qed-.
-