Library CoLoR.Term.WithArity.ANotvar

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2004-12-22
properties of function-headed terms

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig).

Fixpoint notvar (t : term) : Prop :=
  match t with
    | Var _ => False
    | _ => True

Lemma notvar_elim : forall t,
  notvar t -> exists f : Sig, exists ts, t = Fun f ts.

Lemma notvar_var : forall v, ~ notvar (Var v).

Lemma notvar_sub : forall s t, notvar t -> notvar (sub s t).

Lemma notvar_fill : forall c t, notvar t -> notvar (fill c t).

Lemma notvar_fillsub : forall c s t, notvar t -> notvar (fill c (sub s t)).

End S.