fact: Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:= match m with |nil => match k with |nil => True |cons a l => False end |cons b n => match k with |nil => False |cons a l => b[=]a /\ (eq_fm n l) end end.
imports: CoRN.algebra.CSetoids