proposition: Lemma ALFindApp : forall v sub1 sub2, ALFind (sub1 ++ sub2) v = match ALFind sub1 v with | Some t => Some t | None => ALFind sub2 v end.
proof: Proof. induction sub1; simpl; sp. cases_if; auto. Qed.
imports: list Omega