Hi all. I’m trying to define a record type using the dependent Inductive types `dep_T`

and `dep_TT`

. However when I try to construct the record type `Huu`

, it is not able to infer the dependency of `dep_T _ _`

, which is the type of `get_huu`

. What I hope to achieve is, given a term, say `p1`

, and with a proof term `c1 : dep_TT`

, it is able to infer that `get_huu`

is `p2`

and hence fill the placeholders with `b c`

respectively.

But I get the error:

```
Cannot infer this placeholder of type
"Tings" in environment:
Huu : forall n m : Tings, dep_T n m -> Type
n, m : Tings
x : dep_T n m
```

Here’s my code:

```
Inductive Tings := a | b | c | d.
Inductive dep_T : Tings -> Tings -> Type :=
| p1 : dep_T a b
| p2 : dep_T b c
| p3 : dep_T c d.
Inductive dep_TT : forall {w x y z : Tings}, (dep_T w x) ->
(dep_T y z) -> Type :=
| c1 : dep_TT p1 p2
| c2 : dep_TT p2 p3.
Record Huu {n m : Tings}(x : dep_T n m) :=
mk_huu { get_huu :> dep_T _ _; _ : dep_TT x get_huu}.
```