diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 0db172e82a..4825538691 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -56,7 +56,7 @@ Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> Proof with simpl in * ; auto ; simpl_depind. intros Γ Δ τ H. - dependent induction H generalizing Γ Δ. + dependent induction H. destruct Δ... apply weak ; apply ax. @@ -64,7 +64,7 @@ Proof with simpl in * ; auto ; simpl_depind. apply ax. destruct Δ... - specialize (IHterm Γ empty)... + specialize (IHterm Γ empty)... apply weak... apply weak... @@ -81,7 +81,7 @@ Qed. Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; simpl_depind ; auto. intros until 1. - dependent induction H generalizing Γ Δ α β. + dependent induction H. destruct Δ... apply weak ; apply ax. @@ -94,7 +94,7 @@ Proof with simpl in * ; simpl_depind ; auto. apply weak... apply abs... - specialize (IHterm Γ0 (Δ, τ))... + specialize (IHterm Γ0 α β (Δ, τ))... eapply app with τ... Save. |