fact: Fixpoint cvars (c : context) : variables := match c with | Hole => List.nil | Cont H v1 c' v2 => vars_vec v1 ++ cvars c' ++ vars_vec v2 end.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)