fact: Fixpoint unpickle t := match t with | Leaf v => Some (fV v) | Node 0 [::] => Some (fF) | Node 1 [:: t ; t' ] => obind (fun s => obind (fun s' => Some (fImp s s')) (unpickle t')) (unpickle t) | Node 2 [:: t ] => obind (fun s => Some (fAX s)) (unpickle t) | Node 3 [:: t ] => obind (fun s => Some (fAG s)) (unpickle t) | _ => None end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)