alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
definition compose_relations ≝
λC:bishop_set.λU,V:C square → Prop.
λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
definition compose_relations ≝
λC:bishop_set.λU,V:C square → Prop.
λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.