proposition: Lemma sub_comp_single_extend s x v (t : term) : sub (sub_comp s (single x v)) t = sub (extend s x (sub s v)) t.
proof: Proof. apply sub_eq. intros. unfold sub_comp, single, extend. case_beq_nat x x0. rewrite Nat.eqb_refl. refl. rewrite (beq_com beq_nat_ok) in H0. rewrite H0. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)