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