proposition: Lemma rinstId_pure_term : @ren_pure_term id === id .
proof: Proof. exact (feq_trans (rinstInst_pure_term id) instId_pure_term). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms