proposition: Lemma compatible_stable_eq : forall l l', compatible l l' -> stable l l' = true -> l = l'.
proof: Proof. induction 1; simpl; auto. destruct (string_dec s s); try (intuition; fail). case_eq (Ab.eq a1 a2); simpl; try (intros; discriminate). intros Hcmp Hstable ; rewrite IHcompatible; auto. rewrite Ab.eq_sound with (1:=Hcmp); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom