proposition: Theorem compiler_t_term_equiv (c : compiler_t) P i v w : v ⋈ w -> P /X/ (fst P,v) ↓ <-> (i,gc_code c P i) /Y/ (i,w) ↓.
proof: Proof. Proof using . rewrite <- (gc_fst c P i) at 3. apply compiler_t_term_correct. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)