diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 70fb75888e..79d12a0614 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -90,6 +90,28 @@ Proof with simpl in * ; eqns ; eauto with lambda. intro. eapply app... Defined. +Lemma weakening_ctx : forall Γ Δ τ, Γ ; Δ ⊢ τ -> + forall Δ', Γ ; Δ' ; Δ ⊢ τ. +Proof with simpl in * ; eqns ; eauto with lambda. + intros Γ Δ τ H. + + dependent induction H. + + destruct Δ as [|Δ τ'']... + induction Δ'... + + destruct Δ as [|Δ τ'']... + induction Δ'... + + destruct Δ as [|Δ τ'']... + apply abs. + specialize (IHterm Γ (empty, τ))... + + apply abs. + specialize (IHterm Γ (Δ, τ'', τ))... + + intro. eapply app... +Defined. Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; eqns ; eauto. @@ -112,6 +134,8 @@ Proof with simpl in * ; eqns ; eauto. eapply app... Defined. + + (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) Set Implicit Arguments. |