fact: Fixpoint cardinal_e (e:Raw.enumeration D.t) := match e with | Raw.End _ => 0%nat | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e) end.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia