fact: Fixpoint comp (C : context) : context -> context := match C with | Hole => fun E => E | Cont H ts1 D ts2 => fun E => Cont H ts1 (comp D E) ts2 end.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)