proposition: Theorem compiler_t_output_sound' c P i v w i' v' : v ⋈ w -> P /X/ (fst P,v) ~~> (i',v') -> exists w', (i,gc_code c P i) /Y/ (i,w) ~~> (code_end (i,gc_code c P i),w') /\ v' ⋈ w'.
proof: Proof. Proof using . intros H H1. destruct (@compiler_t_output_sound c P i) with (1 := conj H H1) as (w1 & H2 & H3). exists w1; split; auto. rewrite gc_fst, gc_out in H3; auto. apply H1. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)