proposition: Lemma re_override : forall A k m1 (v1 : A) m2 v2 v1' v2', override m1 k v1 = override m2 k v2 -> (v1 = v2 -> v1' = v2') -> override m1 k v1' = override m2 k v2'.
proof: Proof. intros; extensionality x; unfold override in *. apply (f_equal _ _ (fun f => f x)) in H. destruct (x =_? k); auto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)