proposition: Lemma normalise : forall (u v: T), eval (norm u) == eval (norm v) -> eval u == eval v.
proof: Proof. intros u v. rewrite 2 eval_norm. trivial. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)