diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Logic_Type.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index af5b04ed0..fa375ad10 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -94,17 +94,19 @@ End Equality_is_a_congruence. Hints Immediate sym_eqT sym_not_eqT : core v62. -(** This states the replacement of equals by equals in a proposition *) +(** This states the replacement of equals by equals *) -Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y). +Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)y==x -> (P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. -(** not allowed because of dependencies: [[ Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. -]] *) + +Definition eqT_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)y==x -> (P y). +Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. +Defined. (** Some datatypes at the [Type] level *) |