fact: Fixpoint FL (s : form) {struct s} : {fset form} := match s with | fV p => [fset fV p] | fF => [fset fF] | fImp s t => fImp s t |` FL s `|` FL t | [a]s => FL0 a s `|` FL s end with FL0 (a : prog) (s : form) {struct a} : {fset form} := match a with | a + b => [a + b]s |` FL0 a s `|` FL0 b s | a ;; b => [a ;; b]s |` FL0 a [b]s `|` FL0 b s | t?? => [t??]s |` FL t | a^* =>[a^*]s |` FL0 a [a^*]s | pV a => [fset [pV a]s] end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)