proposition: Lemma congr_pure_abs { s0 : pure_term } { t0 : pure_term } : ( s0 = t0 ) -> pure_abs s0 = pure_abs t0 .
proof: Proof. congruence. Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms