blob: c1041d0406df3c596f9451d235df0f52936300ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Import EqNotations.
Record evar_package {T} (v : T) :=
{ val : T;
evar_package_pf : val = v }.
Arguments val {T v} _.
Arguments evar_package_pf {T v} _.
Record evar_rel_package {A} (f : A) B (R : B -> A -> Prop) :=
{ valr : B;
evarr_package_pf : R valr f }.
Arguments valr {A f B R} _.
Arguments evarr_package_pf {A f B R} _.
Record evard_package {s d} (v : s) :=
{ vald : d;
evard_package_pfT : s = d;
evard_package_pf : vald = rew evard_package_pfT in v }.
Arguments vald {s d v} _.
Arguments evard_package_pfT {s d v} _.
Arguments evard_package_pf {s d v} _.
Ltac autosolve else_tac := else_tac ().
|
