proposition: Lemma cast_spec_find : forall A dom₁ dom₂ (Heq : Dom.eq dom₁ dom₂) (m : t A dom₁) x, find x (cast Heq m) = find x m.
proof: Proof. intros. unfold cast, find. simpl. reflexivity. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface