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