fact: Fixpoint equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool := match m, m' with | nil, nil => true | (x,e)::l, (x',e')::l' => match compare x x' with | EQ _ => cmp e e' && equal cmp l l' | _ => false end | _, _ => false end.
imports: Bool OrderedType SMT_classes ProofIrrelevance