proposition: Lemma cast_registeredAs t1 (tt1 : TT t1) Y (R: encodable Y) (cast : projT1 (resType tt1) -> Y) (f:t1) : projT2 (resType tt1) = registerAs cast -> computable (ty:=projT2 (changeResType tt1 (TyB Y))) (insertCast R cast f) -> computable f.
proof: Proof. intros H (s&exts). exists s. induction tt1 in cast,f,H,s,exts |- *. - cbn in H,exts|-*;unfold enc in *. rewrite H. exact exts. - destruct exts as (?&exts). split. assumption. intros x s__x ext__x. specialize (exts x s__x ext__x) as (v &?&exts). exists v. split. tauto. eapply IHtt1_2. all:eassumption. Qed.
imports: String