proposition: Fact fol_bin_sem_ext b A A' B B' : (A <-> A') -> (B <-> B') -> (fol_bin_sem b A B <-> fol_bin_sem b A' B').
proof: Proof. intros E1 E2; destruct b; simpl; tauto. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)