Define utilities
Substitute bullet for Case tactic
Substitute Forall2 for List_P2'
Remove Prop_Ind
Substitute FJ_util for FJ_tactics