proposition: Lemma cast_computable X Y `{encodable Y} (cast : X -> Y) : let _ := registerAs cast in computable cast.
proof: Proof. cbn. pose (t:=lam 0). computable using t. Qed.
imports: MetaCoq.Template.All Strings.Ascii Undecidability.L.Tactics(Lproc Computable Lsimpl Lbeta Lrewrite) Ring Arith Lia