A framework is given to formulate an assurance case as a pair of a formal theory (vocabulary and basic assumptions; a formal model) and a proof in it, thus objectifying ontological presumptions separately from reasoning based on it. Our formulation is given in Agda, a programming and proof description language based on constructive type theory. Emphasis on explicit presumptions improves upon currently prevailing structured-argument notations such as GSN and CAE. Changes and vagueness in modern complex systems must be reflected by rebuttals to their assurance cases. We sketch our approach to formulate rebuttals to that end, where objectification of ontological presumptions works effectively.