proposition: Lemma compatible_widen : forall l l', compatible l (widen l l').
proof: Proof. induction l; simpl; try constructor. intros l'; destruct a as [s v]; constructor; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom