proposition: Lemma instId_pure_term : subst_pure_term (pure_var ) === id .
proof: Proof. exact ((fun x => idSubst_pure_term (pure_var ) (fun n => eq_refl) (id x))). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms