proposition: Lemma hlist_erase_hlist_gen : forall A B ls (f : A -> B), hlist_erase (hlist_gen f ls) = map f ls.
proof: Proof. induction ls; simpl; intros; f_equal; auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms