proposition: Lemma hole_l_varUD : forall E k p, p < k -> E |= p :! -> (initialSeg E k ++ finalSeg E (S k)) |= p :! .
proof: Proof. intros. apply (proj1 (proj2 (equiv_hole_l E H))); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)