proposition: Lemma C2M : forall p q : nat, gencode (Call_C p q) -> gencode (Call_M p).
proof: Proof. refine (fun p q g => match g with | gencode_intro c s => gencode_intro _ c _ end). constructor 1. inversion_clear s. auto with arith. Qed.
imports: Constants monoid spec machine Wf_compl Plus Mult Lt Mult_compl euclid two_power