fact: Definition sym_match s th1 th2 := let: Sym si sj sk := s in let: (ri, rj, rk) := (th_bbox th1, th_dim th1) in let is_sym r s := uniq s && all (gtn r) s in let match_cl cl2 := let: (i2, j2, kvs2) := cl2 in let ij := (nth ri si i2, nth rj sj j2) in let match_lit kvs1 kv := (nth rk sk kv.1, kv.2) \in kvs1 in let match_cl1 cl1 := let: (ij1, kvs1) := cl1 in (ij1 == ij) && all (match_lit kvs1) kvs2 in uniq (unzip1 kvs2) && has match_cl1 th1 in [&& is_sym ri si, is_sym rj sj, is_sym rk sk & all match_cl th2].
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)