proposition: Lemma compatible_trans : forall A l l' l'', @compatible A l l' -> compatible l' l'' -> compatible l l''.
proof: Proof. intros A l l' l'' H; generalize l''; clear l''; induction H; intros l'' H'; inversion H'; constructor; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom