proposition: Lemma ALFindMapNone : forall {KA KB VA VB : Type} (DKA : Deq KA) (DKB : Deq KB) (fk : KA -> KB) (fv : VA -> VB), injective_fun fk -> forall (sub : AssocList KA VA) v, ALFind DKA sub v = None -> ALFind DKB (ALMap fk fv sub) (fk v) = None.
proof: Proof. introv Hik. induction sub;simpl; introv Heq; sp; allsimpl;[]. cases_ifd Hd; cpx. + f_equal. apply Hik in Hdt. destruct Hdt. rewrite DeqTrue in Heq. invertsn Heq. + apply IHsub. revert Heq. cases_ifd Hdd; subst; cpx. Qed.
imports: list Omega