proposition: Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v.
proof: Proof. intros u v H. apply normalise. apply compare_reflect_eq. apply H. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)