Library Must.Main

Bar induction

From Must Require Bar.

Must preorder.

From Must Require TransitionSystems.

From Must Require Must.

From Must Require Soundness.

From Must Require Completeness.

From Must Require Lift.

From Must Require Equivalence.

From Must Require Normalisation.

Example with ACCS.

From Must Require ACCSInstance.