Unsound STLC axiom

[Pat-Lafon]

The following axiom

underapproximation_type/data/predefined/axioms.ml

Lines 497 to 502 in 94d0f05

	let[@axiom] stlc_abd_typing_rev (gamma : stlc_tyctx) (v : stlc_term)
	(tau : stlc_ty) (ty : stlc_ty) (body : stlc_term) (body_ty : stlc_ty)
	(gamma1 : stlc_tyctx) =
	(typing gamma v tau && stlc_abs_ty v ty && stlc_abs_body v body
	&& stlc_tyctx_hd gamma1 ty && stlc_tyctx_tl gamma1 gamma)
	#==> (typing gamma1 body body_ty)

Does not have any constraints on what body_ty can be and is unsound.

I would propose the following axiom instead, which I've checked against my coq definition.

let[@axiom] stlc_abd_typing_rev (gamma : stlc_tyctx) (v : stlc_term)
    (tau : stlc_ty) (ty : stlc_ty) (body : stlc_term) (body_ty : stlc_ty)
    (gamma1 : stlc_tyctx) =
  (typing gamma v tau && stlc_abs_ty v ty && stlc_abs_body v body
 && stlc_ty_arr1 tau ty && stlc_ty_arr2 tau body_ty && stlc_tyctx_hd gamma1 ty
 && stlc_tyctx_tl gamma1 gamma)
  #==> (typing gamma1 body body_ty)