✐‹creator "Kevin Kappelmann"› theory Transport_White_Box imports Transport_Equality Transport_Existential_Quantifier Transport_Galois_Relator_Properties Transport_Universal_Quantifier begin paragraph ‹Summary› text ‹Theorems for white-box transports.› context galois begin (*TODO: for the Galois relator, many assumptions needed for the white-box transport theorems of the logical connectives become vacuous. Example:*) notepad begin print_statement Fun_Rel_imp_eq_restrict_if_right_unique_onI [of "in_field (≤⇘L⇙)" "(⇘L⇙⪅)" "in_field (≤⇘R⇙)"] have "((⇘L⇙⪅) ⇛ (⟶)) (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙))" by (intro Fun_Rel_relI) auto end end end