Commit c059a9d6 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Remove unused context variables

parent c7270df2
......@@ -109,7 +109,7 @@ def fun_eq : L : sorts -> B : sort -> (terms L -> term B) -> (terms L -> term B)
def eq_fun_eq : L : sorts -> B : sort -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_sort B b --> fol.all_elim B (x => eq B x x) (eq_refl B) (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_sort A L) B f -->
[A,L,B,f] eq_fun_eq (fol.cons_sort A L) B f -->
fol.all_intro A (x => all A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l)))))
(x =>
fol.all_intro A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))))
......
......@@ -165,12 +165,12 @@ def nall_aux_type : sorts -> Type.
[A,As] nall_aux_type (cons_sort A As) --> term A -> nall_aux_type As.
def nall_aux : As : sorts -> nall_aux_type As -> prop.
[P] nall_aux nil_sort --> P => P.
[A,As,P] nall_aux (cons_sort A As) --> P => all A (a => nall_aux As (P a)).
[] nall_aux nil_sort --> P => P.
[A,As] nall_aux (cons_sort A As) --> P => all A (a => nall_aux As (P a)).
def nex_aux : As : sorts -> nall_aux_type As -> prop.
[P] nex_aux nil_sort --> P => P.
[A,As,P] nex_aux (cons_sort A As) --> P => ex A (a => nex_aux As (P a)).
[] nex_aux nil_sort --> P => P.
[A,As] nex_aux (cons_sort A As) --> P => ex A (a => nex_aux As (P a)).
(; nall_aux2 [B₁; …; Bₘ] n A₁ … Aₙ = nall_aux [B₁; …; Bₘ; A₁; …; Aₙ] ;)
(; nall_aux2_type Bs n A₁ … Aₙ = nall_aux_type (Bs^As) -> prop ;)
......
......@@ -182,11 +182,11 @@ def f_equal_fun_n : L' : fol.sorts ->
L : fol.sorts ->
certificates L ->
f_equal_T L'.
[L,B,f,as,bs,cs]
[L,cs]
f_equal_fun_n fol.nil_sort L cs
-->
f_equal_fun_on_goal L cs
[A,As,L,B,f,as,bs,cs]
[A,As,L,cs]
f_equal_fun_n (fol.cons_sort A As) L cs
-->
c : tactic =>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment