fact: Fixpoint eqf (s t : form) := match s, t with | fV p,fV q => p == q | fF,fF => true | fImp s1 t1,fImp s2 t2 => eqf s1 s2 && eqf t1 t2 | [a]s, [b]t => eqp a b && eqf s t | _,_ => false end with eqp (p q : prog) := match p,q with | pV a,pV b => a == b | a1 ;; b1, a2 ;; b2 => eqp a1 a2 && eqp b1 b2 | a1 + b1, a2 + b2 => eqp a1 a2 && eqp b1 b2 | a^*,b^* => eqp a b | s??,t?? => eqf s t | p^^,q^^ => eqp p q | _,_ => false end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)