fact: Axiom add_test_constraint_left_monotonic : forall neg v1 v2 v1' v2' v v', add_test_constraint_left neg v1 v2 = Some v -> add_test_constraint_left neg v1' v2' = Some v' -> thinner v1 v1' -> thinner v2 v2' -> thinner v v'.
imports: syntax little denot Bool List String ZArith axiom