proposition: Theorem is_nil_id : forall (d : nat) (a : mon d), a = is_nil d a.
proof: Proof. intros d a; elim a; simpl in |- *; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)