proposition: Lemma notvar_elim : forall t, notvar t -> exists f : Sig, exists ts, t = Fun f ts.
proof: Proof. intro t. case t; simpl; intros. contr. exists f. exists t0. refl. Qed.
imports: CoLoR(LogicUtil ATerm AContext ASubstitution)