Mcltt.Core.Completeness.Consequences.Inversions
From Coq Require Import RelationClasses.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.Consequences.Types.
From Mcltt.Core Require Export SystemOpt CoreInversions.
Import Domain_Notations.
(* Corollary wf_zero_inversion' : forall Γ A, *)
(* {{ Γ ⊢ zero : A }} -> *)
(* exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
(* Proof with mautosolve 4. *)
(* intros * typ_subsumption_left_nat... *)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_zero_inversion' : mcltt. *)
(* Corollary wf_succ_inversion' : forall Γ A M, *)
(* {{ Γ ⊢ succ M : A }} -> *)
(* {{ Γ ⊢ M : ℕ }} /\ exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
(* Proof with mautosolve. *)
(* intros * ? []%typ_subsumption_left_nat*)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_succ_inversion' : mcltt. *)
(* Corollary wf_fn_inversion' : forall {Γ A M C}, *)
(* {{ Γ ⊢ λ A M : C }} -> *)
(* exists B, {{ Γ, A ⊢ M : B }} /\ exists i, {{ Γ ⊢ Π A B ≈ C : Type@i }}. *)
(* Proof with mautosolve. *)
(* intros * ? [? []%typ_subsumption_left_pi]*)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_fn_inversion' : mcltt. *)
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.Consequences.Types.
From Mcltt.Core Require Export SystemOpt CoreInversions.
Import Domain_Notations.
(* Corollary wf_zero_inversion' : forall Γ A, *)
(* {{ Γ ⊢ zero : A }} -> *)
(* exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
(* Proof with mautosolve 4. *)
(* intros * typ_subsumption_left_nat... *)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_zero_inversion' : mcltt. *)
(* Corollary wf_succ_inversion' : forall Γ A M, *)
(* {{ Γ ⊢ succ M : A }} -> *)
(* {{ Γ ⊢ M : ℕ }} /\ exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
(* Proof with mautosolve. *)
(* intros * ? []%typ_subsumption_left_nat*)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_succ_inversion' : mcltt. *)
(* Corollary wf_fn_inversion' : forall {Γ A M C}, *)
(* {{ Γ ⊢ λ A M : C }} -> *)
(* exists B, {{ Γ, A ⊢ M : B }} /\ exists i, {{ Γ ⊢ Π A B ≈ C : Type@i }}. *)
(* Proof with mautosolve. *)
(* intros * ? [? []%typ_subsumption_left_pi]*)
(* Qed. *)
(* [export] *)
(* Hint Resolve wf_fn_inversion' : mcltt. *)