fact: Fixpoint unpicklef 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')) (unpicklef t')) (unpicklef t) | Node 2 [:: p ; t ] => obind (fun q => obind (fun s => Some (fAX q s)) (unpicklef t)) (unpicklep p) | _ => None end with unpicklep t := match t with | Leaf v => Some (pV v) | Node 0 [:: t ; t'] => obind (fun p => obind (fun p' => Some (pSeq p p')) (unpicklep t')) (unpicklep t) | Node 1 [:: t ; t'] => obind (fun p => obind (fun p' => Some (pCh p p')) (unpicklep t')) (unpicklep t) | Node 2 [:: t] => obind (fun p => Some (pStar p)) (unpicklep t) | Node 3 [:: s] => obind (fun s => Some (pTest s)) (unpicklef s) | _ => None end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)