Change weight definition from Dyckhoff and Negri's to Pitts'

theories/iSL/Formulas.v

@@ -105,7 +105,7 @@ Fixpoint weight (φ : form) : nat := match φ with
 | ⊥ => 1
 | Var _ => 1
 | φ ∧ ψ => 2 + weight φ + weight ψ
-| φ ∨ ψ => 3 + weight φ + weight ψ
+| φ ∨ ψ => 1 + weight φ + weight ψ
 | φ → ψ => 1 + weight φ + weight ψ
 | □φ => 1 + weight φ
 end.

theories/iSL/Order.v

@@ -413,3 +413,8 @@ apply Nat.pow_le_mono_r with (a := 5) in Hle; lia.
 Qed.
 
 Hint Resolve pointed_env_order_bot_L : order.
+
+Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b).
+Proof. destruct a; simpl; lia. Qed.
+
+Hint Resolve weight_or_bot : order.