proposition: Lemma instId_term : subst_term (poly_var ) (var ) === id .
proof: Proof. exact ((fun x => idSubst_term (poly_var ) (var ) (fun n => eq_refl) (fun n => eq_refl) (id x))). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms