proposition: Lemma context_closed_fun : forall R, context_closed R -> forall f i v1 t u j v2 (e : i+S j=arity f), R t u -> R (Fun f (Vcast (Vapp v1 (Vcons t v2)) e)) (Fun f (Vcast (Vapp v1 (Vcons u v2)) e)).
proof: Proof. intros. set (c := Cont f e v1 Hole v2). change (R (fill c t) (fill c u)). apply H. hyp. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)