proposition: Lemma rinstId_poly_type : @ren_poly_type id === id .
proof: Proof. exact (feq_trans (rinstInst_poly_type id) instId_poly_type). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms