fact: Fixpoint picklef (s : form) := match s with | fV v => Leaf v | fF => Node 0 [::] | fImp s t => Node 1 [:: picklef s ; picklef t] | fAX p s => Node 2 [:: picklep p ; picklef s] end with picklep (p : prog) := match p with | pV v => Leaf v | pSeq p1 p2 => Node 0 [:: picklep p1 ; picklep p2] | pCh p1 p2 => Node 1 [:: picklep p1 ; picklep p2] | pStar p => Node 2 [:: picklep p] | pTest s => Node 3 [:: picklef s] end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)