λp. l;𝐞 = p.
definition preterm_node_1 (l): preterm → preterm ≝
- λt,p. ∃∃q. q ϵ⬦ t & l;q = p.
+ λt,p. ∃∃q. q ϵ t & l;q = p.
definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
λt1,t2,p.
- ∨∨ ∃∃q. q ϵ⬦ t1 & l1;q = p
- | ∃∃q. q ϵ⬦ t2 & l2;q = p.
+ ∨∨ ∃∃q. q ϵ t1 & l1;q = p
+ | ∃∃q. q ϵ t2 & l2;q = p.
interpretation
"outer variable reference by depth (preterm)"
(* Basic Inversions *********************************************************)
lemma preterm_in_root_inv_lcons_oref:
- ∀p,l,n. l;p ϵ▵ #n →
+ ∀p,l,n. l;p ϵ ▵#n →
∧∧ 𝗱❨n❩ = l & 𝐞 = p.
#p #l #n * #q
<list_append_lcons_sn #H0 destruct -H0
qed-.
lemma preterm_in_root_inv_lcons_iref:
- ∀t,p,l,n. l;p ϵ▵ 𝛗n.t →
- ∧∧ 𝗱❨n❩ = l & p ϵ▵ t.
+ ∀t,p,l,n. l;p ϵ ▵𝛗n.t →
+ ∧∧ 𝗱❨n❩ = l & p ϵ ▵t.
#t #p #l #n * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
lemma preterm_in_root_inv_lcons_abst:
- ∀t,p,l. l;p ϵ▵ 𝛌.t →
- ∧∧ 𝗟 = l & p ϵ▵ t.
+ ∀t,p,l. l;p ϵ ▵𝛌.t →
+ ∧∧ 𝗟 = l & p ϵ ▵t.
#t #p #l * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
lemma preterm_in_root_inv_lcons_appl:
- ∀u,t,p,l. l;p ϵ▵ @u.t →
- ∨∨ ∧∧ 𝗦 = l & p ϵ▵ u
- | ∧∧ 𝗔 = l & p ϵ▵ t.
+ ∀u,t,p,l. l;p ϵ ▵@u.t →
+ ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
+ | ∧∧ 𝗔 = l & p ϵ ▵t.
#u #t #p #l * #q
<list_append_lcons_sn * * #r #Hr #H0 destruct
/4 width=2 by ex_intro, or_introl, or_intror, conj/