proposition: Lemma ALFindEndoMapSome : forall {KA VA VB: Type} (DKA : Deq KA) (fk : KA -> KA) (fv : VA -> VB), injective_fun fk -> forall (sub : AssocList KA VA) v, ALFind DKA sub v = None -> ALFind DKA (ALMap fk fv sub) (fk v) = None.
proof: Proof. intros. eapply ALFindMapNone; eauto. Qed.
imports: list Omega