proposition: Lemma alist_find_alt (m: alist) : forall k: K, alist_find k m = alist_find' k m.
proof: Proof. induction m; intuition. unfold alist_find', compose. simpl. destruct (k ?[ R ] a0) eqn:Heq; [intuition|]. rewrite IHm. reflexivity. Qed.
imports: Coq.Classes.RelationClasses Coq.Lists.List ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Structures.Maps ExtLib.Structures.Monad ExtLib.Structures.Reducible ExtLib.Structures.Functor Coq(Basics) ExtLib(Extras OptionMonad)