proposition: Lemma McCarthy_fix : forall n, mcCarthy n = McCarthy mcCarthy n.
proof: Proof. Proof using. apply (proj1 (McCarthy_fix_post)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat