proposition: Lemma cons_cardinal_e : forall m e, cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat.
proof: Proof. induction m; simpl; intros; auto. rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia