diff --git a/theories/Core/Equivocation.v b/theories/Core/Equivocation.v
index 7d38be62..a0a5c1cc 100644
--- a/theories/Core/Equivocation.v
+++ b/theories/Core/Equivocation.v
@@ -703,11 +703,11 @@ Lemma from_send_to_from_sent_argument
   `{HasBeenSentCapability}
   (P : state vlsm -> Prop)
   (P_stable : forall s l oim s' oom,
-    input_valid_transition pre_vlsm l (s, oim) (s', oom) ->
+    input_constrained_transition vlsm l (s, oim) (s', oom) ->
     P s -> P s')
   (msg : message)
   (send_establishes_P : forall s l oim s',
-    input_valid_transition pre_vlsm l (s, oim) (s', Some msg) ->
+    input_constrained_transition vlsm l (s, oim) (s', Some msg) ->
     P s') :
   forall s,
     valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s ->
diff --git a/theories/Core/Equivocation/TraceWiseEquivocation.v b/theories/Core/Equivocation/TraceWiseEquivocation.v
index 55929783..d9f57b50 100644
--- a/theories/Core/Equivocation/TraceWiseEquivocation.v
+++ b/theories/Core/Equivocation/TraceWiseEquivocation.v
@@ -221,7 +221,7 @@ Qed.
 
 Lemma transition_is_equivocating_tracewise_char
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (v : validator)
   : is_equivocating_tracewise_no_has_been_sent s' v ->
     is_equivocating_tracewise_no_has_been_sent s v \/
@@ -245,7 +245,7 @@ Qed.
 
 Lemma transition_receiving_no_sender_reflects_is_equivocating_tracewise
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   (v : validator)
   : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v.
@@ -336,7 +336,7 @@ Qed.
 
 Lemma input_valid_transition_receiving_no_sender_reflects_equivocating_validators
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   : equivocating_validators s' ⊆ equivocating_validators s.
 Proof.
@@ -357,7 +357,7 @@ Qed.
 
 Lemma composite_transition_no_sender_equivocators_weight
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   : (equivocation_fault s' <= equivocation_fault s)%R.
 Proof.
diff --git a/theories/Core/Equivocation/WitnessedEquivocation.v b/theories/Core/Equivocation/WitnessedEquivocation.v
index 12893f78..7fed6785 100644
--- a/theories/Core/Equivocation/WitnessedEquivocation.v
+++ b/theories/Core/Equivocation/WitnessedEquivocation.v
@@ -168,7 +168,7 @@ Qed.
 *)
 Lemma equivocating_validators_step_update
     l s om s' om'
-    (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+    (Ht : input_constrained_transition Free l (s, om) (s', om'))
     v
     : v ∈ equivocating_validators s' ->
       v ∈ equivocating_validators s \/
diff --git a/theories/Core/HistoryVLSM.v b/theories/Core/HistoryVLSM.v
index 9d532871..bae25e6a 100644
--- a/theories/Core/HistoryVLSM.v
+++ b/theories/Core/HistoryVLSM.v
@@ -111,7 +111,7 @@ Lemma composite_valid_transition_reflects_rechability :
   forall l s1 iom s2 oom,
   composite_valid_transition IM l s1 iom s2 oom ->
   valid_state_prop RFree s2 ->
-  input_valid_transition RFree l (s1, iom) (s2, oom).
+  input_constrained_transition Free l (s1, iom) (s2, oom).
 Proof.
   intros * Hnext Hs2; revert l s1 iom oom Hnext.
   induction Hs2 using valid_state_prop_ind; intros * Hnext.
@@ -140,7 +140,7 @@ Proof.
           apply f_equal with (f := fun s => s j) in Heqs'.
           by state_update_simpl.
       }
-      assert (Hss1 : input_valid_transition RFree (existT i li)
+      assert (Hss1 : input_constrained_transition Free (existT i li)
                   (state_update IM s j (s1 j), om) (s1, om')).
       {
         repeat split; [by apply IHHs2 | by apply any_message_is_valid_in_preloaded | ..]
@@ -175,7 +175,7 @@ Lemma composite_valid_transitions_from_to_reflects_reachability :
   valid_state_prop RFree s' -> finite_valid_trace_from_to RFree s s' tr.
 Proof.
   induction 1; intros; [by constructor |].
-  assert (Hitem : input_valid_transition RFree (l item) (s', input item)
+  assert (Hitem : input_constrained_transition Free (l item) (s', input item)
                           (destination item, output item))
     by (apply composite_valid_transition_reflects_rechability; done).
   eapply finite_valid_trace_from_to_app.
diff --git a/theories/Core/ProjectionTraces.v b/theories/Core/ProjectionTraces.v
index 6709e4b4..a6965f58 100644
--- a/theories/Core/ProjectionTraces.v
+++ b/theories/Core/ProjectionTraces.v
@@ -201,8 +201,7 @@ Lemma pre_loaded_with_all_messages_projection_input_valid_transition_eq
   (s1 s2 : composite_state IM)
   (om1 om2 : option message)
   (l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)))
-  (Ht : input_valid_transition
-          (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) l (s1, om1) (s2, om2))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
   (Hl : projT1 l = j)
   : input_constrained_transition (IM (projT1 l))
       (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2).
@@ -220,8 +219,7 @@ Lemma pre_loaded_with_all_messages_projection_input_valid_transition_neq
   [s1 s2 : composite_state IM]
   [om1 om2 : option message]
   [l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))]
-  (Ht : input_valid_transition
-          (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) l (s1, om1) (s2, om2))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
   [i : index]
   (Hi : i <> projT1 l)
   : s1 i = s2 i.
diff --git a/theories/Core/SubProjectionTraces.v b/theories/Core/SubProjectionTraces.v
index 3812a1b0..38c5150b 100644
--- a/theories/Core/SubProjectionTraces.v
+++ b/theories/Core/SubProjectionTraces.v
@@ -1553,7 +1553,7 @@ Qed.
   Note that, in general, this is not trace-equivalent with the directly obtained
   [projection_induced_validator] of the constrained composition to the corresponding
   component, as the intermediate induced projection might generate more
-  [input_valid_transitions] to be considered as a basis for the next projection.
+  [input_valid_transition]s to be considered as a basis for the next projection.
 *)
 
 Definition sub_label_element_project
diff --git a/theories/Examples/Tutorial/Multiply.v b/theories/Examples/Tutorial/Multiply.v
index fe5a8cd6..b96efbce 100644
--- a/theories/Examples/Tutorial/Multiply.v
+++ b/theories/Examples/Tutorial/Multiply.v
@@ -353,7 +353,7 @@ Qed.
 *)
 
 Example doubling_example_constrained_transition :
-  input_valid_transition (pre_loaded_with_all_messages_vlsm doubling_vlsm) multiply_label
+  input_constrained_transition doubling_vlsm multiply_label
    (3, Some 3) (0, Some 6).
 Proof.
   apply (finite_valid_trace_from_to_last_transition