proposition: Lemma congr_abs { s0 : poly_type } { s1 : term } { t0 : poly_type } { t1 : term } : ( s0 = t0 ) -> ( s1 = t1 ) -> abs s0 s1 = abs t0 t1 .
proof: Proof. congruence. Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms