gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
Require Import List Nat Ensembles Image.
Import  ListNotations.


Notation empty := (Empty_set _).
Notation single := (Singleton _).
Notation union := (Union _).

Definition bigcup {T} (X : Ensemble (Ensemble T)) : Ensemble T :=

gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.
Require Import Bool Nat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Class lattice := Lattice {
  base : finType;
  meet : base -> base -> base;

gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.
Require Import Bool.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Class poSet := PoSet {
  base : finType;

gaxiiiiiiiiiiii

From mathcomp Require Export fintype finset ssrbool ssreflect eqtype.


Module Type SIG.
  Parameter T : finType.
  Parameter A : {set T}.
  Parameter F : {set T} -> {set T}.
  Parameter mono : forall (X Y : {set T}), X \subset Y -> F X \subset F Y.
End SIG.

gaxiiiiiiiiiiii

From mathcomp Require Export fintype finset ssrbool ssreflect.



Module Type FinTypeSig.
  Parameter T : finType.
End FinTypeSig.

Module Type ArgFrame (FTS : FinTypeSig).
  Import FTS.

gaxiiiiiiiiiiii

Require Import Ensembles.
From mathcomp Require Import ssreflect.

Arguments Singleton {U}.
Arguments Union {U}.
Arguments Setminus {U}.
Arguments Included {U}.
Arguments Couple {U}.
Arguments Empty_set {U}.

gaxiiiiiiiiiiii

Require Import List Bool  Classical.

Import ListNotations.
From mathcomp Require Import ssreflect ssrbool.
Require Import Ensembles ProofIrrelevance Classical_sets.



Definition var := nat.
Variable fls tru : var.

gaxiiiiiiiiiiii

Require Import List.
Import ListNotations.

Variable var : Type.
Variable tru fls : var.

Inductive prop :=
  | Var : var -> prop
  | Not : prop -> prop
  | And : prop -> prop -> prop

gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.


Variables argument position : finType.
Definition A := [set : argument].
Definition X := [set : position].

Definition Rel := rel position.

Axiom axiomA : 0 < #|argument|.

gaxiiiiiiiiiiii

Require Export Classical.

Module ACTL.
Section Def.


Context {state action : Set} {trans : state -> action -> state -> Prop}
        {tau : action} {tau_eq : forall  s s', trans s tau s' <->  s = s'}.