fact: Fixpoint fsubst (f : formula R) (s : nat * term R) := match f with | Bool _ => f | 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%T.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)