fact: Definition check_congr_pred (PA:_lit) (PB:_lit) (eqs:list (option _lit)) := let xPA := Lit.blit PA in let xPB := Lit.blit PB in match get_form xPA, get_form xPB with | Form.Fatom pa, Form.Fatom pb => match get_atom pa, get_atom pb with | Atom.Abop o1 a1 a2, Atom.Abop o2 b1 b2 => if Atom.bop_eqb o1 o2 then build_congr eqs (a1::a2::nil) (b1::b2::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil) else C._true | Atom.Auop o1 a, Atom.Auop o2 b => if Atom.uop_eqb o1 o2 then build_congr eqs (a::nil) (b::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil) else C._true | Atom.Aapp p a, Atom.Aapp p' b => if p =? p' then build_congr eqs a b (Lit.nlit xPA :: Lit.lit xPB :: nil) else C._true | _, _ => C._true end | _, _ => C._true end.
imports: Bool List Int63 PArray State SMT_terms