proposition: Lemma lift_normalise {S} {H : AAC_lift S R} : forall (u v: T), (let x := norm u in let y := norm v in S (eval x) (eval y)) -> S (eval u) (eval v).
proof: Proof. destruct H. intros u v; simpl; rewrite 2 eval_norm. trivial. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)