fact: Fixpoint fsubst (f : formula T) (s : nat * term T) := match f with | Bool _ => f | (t1 == t2) => (tsubst t1 s == tsubst t2 s) | (t1 <% t2) => (tsubst t1 s <% tsubst t2 s) | (t1 <=% t2) => (tsubst t1 s <=% tsubst t2 s) | (Unit t1) => Unit (tsubst t1 s) | (f1 /\ f2) => (fsubst f1 s /\ fsubst f2 s) | (f1 \/ f2) => (fsubst f1 s \/ fsubst f2 s) | (f1 ==> f2) => (fsubst f1 s ==> fsubst f2 s) | (~ f1) => (~ fsubst f1 s) | ('exists 'X_i, f1) => ('exists 'X_i, if i == s.1 then f1 else fsubst f1 s) | ('forall 'X_i, f1) => ('forall 'X_i, if i == s.1 then f1 else fsubst f1 s) end%oT.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)