1 2 3 4 5
Local Obligation Tactic := idtac. Definition a := 1. Definition b := 1. Definition c := 1. Definition d := 1.