proposition: Lemma ext_rel_helper X `(H:encodable X) (x:X) (inst : computable x) (R: term -> term -> Prop) u: R (enc x) u -> R (@ext _ _ _ inst) u.
proof: Proof. now rewrite ext_is_enc. Qed.
imports: Undecidability.L(Tactics.Computable Lproc Lbeta)