How would I go about proving

```
forall cf : checker_flags,
normalizing_flags ->
forall (guard : abstract_guard_impl) (_Σ : referenced_impl_ext),
axiom_free _Σ ->
let Σ := referenced_impl_env_ext _Σ in
let Σ' := global_env_add Σ.1 (make_fresh_name Σ, InductiveDecl False_mib) in
let Σext := (Σ', Σ.2) in
wf_ext Σext ->
(forall (Γ : context) (t : term), welltyped _Σ Γ t -> Acc (cored _Σ Γ) t) ->
forall (Γ : context) (t : term), welltyped Σext Γ t -> Acc (cored Σext Γ) t
```

without assuming `normalisation`

? (Unqualified definitions are located as they would be if this were to be inserted as a goal at the end of `safechecker/theories/PCUICConsistency.v`

)

Last updated: Jul 24 2024 at 12:02 UTC