Library Tactics
Tactics for closedness and abstractions
Lemma
proc_closed
p
:
proc
p
→
closed
p
.
Lemma
proc_lambda
p
:
proc
p
→
lambda
p
.
Simplifying goals
Solving reductions
Solving equivalences
Lemma
equiv_trans_r
(
s
t
t'
:
term
) :
t
==
t'
→
s
t
==
s
t'
.
Lemma
database_dummy
:
I
I
I
I
I
==
I
I
I
I
I
.