"application (prototerm)"
'At u t = (prototerm_node_2 label_S label_A u t).
+(* Basic constructions *******************************************************)
+
+lemma in_comp_iref (t) (q) (n):
+ q ฯต t โ ๐ฑnโ๐บโq ฯต ๐n.t.
+/2 width=3 by ex2_intro/ qed.
+
(* Basic Inversions *********************************************************)
+lemma in_comp_inv_iref (t) (p) (n):
+ p ฯต ๐n.t โ
+ โโq. ๐ฑnโ๐บโq = p & q ฯต t.
+#t #p #n * #q #Hq #Hp
+/2 width=3 by ex2_intro/
+qed-.
+(*
lemma prototerm_in_root_inv_lcons_oref:
โp,l,n. lโp ฯต โต#n โ
โงโง ๐ฑn = l & ๐ = p.
<list_append_lcons_sn #H0 destruct
/4 width=2 by ex_intro, or_introl, or_intror, conj/
qed-.
+*)