(* PROPER CONDITION FOR PROTOTERM *******************************************)
-(* Constructions with inner condition for prototerm *************************)
+(* Constructions with pic ***************************************************)
lemma term_proper_outer (t):
t β§Έβ¬ π β t Ο΅ π.