proposition: Lemma Vmonotone_context_closed : forall R, (forall f : Sig, Vmonotone (Fun f) R R) <-> context_closed R.
proof: Proof. split; intro. unfold context_closed. induction c; simpl; intros. hyp. apply H. auto. unfold Vmonotone, Vmonotone_i, RelUtil.monotone. intros. set (c := Cont f H0 vi Hole vj). change (R (fill c x) (fill c y)). apply H. hyp. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)