q Ļµ t ā š±nāšŗāq Ļµ šn.t.
/2 width=3 by ex2_intro/ qed.
-(* Basic Inversions *********************************************************)
+(* Basic inversions *********************************************************)
lemma in_comp_inv_iref (t) (p) (n):
p Ļµ šn.t ā