fact: Record demo (S T : {fset clause}) := Demo { demoT : forall C, C \in T -> lcons C; demoSsubT : {subset S <= T}; demo1 : AXn_complete S; demo2 s t L : L \in S -> fAX (fAU s t)^+ \in L -> fulfillsAU S T s t L; demo3 s t L : L \in S -> fAX (fAR s t)^- \in L -> fulfillsAR S T s t L}.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)