fact: Fixpoint fill (c : context) (t : term) : term := match c with | Hole => t | Cont H v1 c' v2 => Fun _ (Vcast (Vapp v1 (Vcons (fill c' t) v2)) H) end.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)