(* *)
(**************************************************************************)
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
include "basic_2/reducibility/lfpr.ma".
(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)