Theory Product_Type_Ext

(* Title: Examples/SML_Relativization/Foundations/Product_Type_Ext.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Extension of the theory \<^text>‹Product_Type_Ext››
theory Product_Type_Ext
  imports Main
begin

context
  includes lifting_syntax
begin

lemma Sigma_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows 
    "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B))
      Sigma Sigma"
  unfolding Sigma_def by transfer_prover

end

text‹\newpage›

end