Jason Gross (Nov 24 2022 at 00:07): Jason Gross (Nov 24 2022 at 00:07):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: Apr 19 2024 at 19:02 UTC