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