proposition: Lemma cont_case : forall c, c = Hole \/ exists d, exists f, exists i, exists vi, exists j, exists vj, exists e : i + S j = arity f, c = comp d (Cont e vi Hole vj).
proof: Proof. induction c. auto. right. destruct IHc. subst. exists Hole. exists f. exists i. exists t. exists j. exists t0. exists e. refl. decomp H. subst. exists (Cont e t x t0). exists x0. exists x1. exists x2. exists x3. exists x4. exists x5. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)