Extension function rewriting lemmas

This file contains lemmas that rewrite Cedar extension function definitions into equivalent forms that are easier to reason about in SymCC proofs.

theorem Cedar.Thm.toDate_eq_smod (datetime : Spec.Ext.Datetime) : datetime.toDate = have millisPerDayI64 := Int64.ofIntChecked Spec.Ext.Datetime.MILLISECONDS_PER_DAY toDate_eq_smod._proof_1; Spec.Ext.Datetime.datetime? (datetime.val.toInt - (datetime.val.smod millisPerDayI64).toInt)

Equivalent formulation of toDate using Int64.smod, useful for symbolic compilation.