Hello! I’m new to Coq and to writing machine-verified proofs in general – I just started at this yesterday – and have occasionally been stymied because I know what I want to do but have no idea about the basic syntax to express it. I’m currently working on an exercise to prove a relationship between two functions and need to gather some information out of a hypothesis I have. At present, my hypothesis reads

```
H : match typecheck e with
| Just TBool => Just TBool
| _ => Nothing
end = Just t
```

Here, `Just`

and `Nothing`

are constructors for my own little `option`

-like type (because I made my own to learn how such things are defined). In case it’s relevant, the definition is

```
Inductive maybe {A:Type} : Type :=
| Just : A -> @maybe A
| Nothing : @maybe A
.
```

I would expect to be able to learn the following from hypothesis `H`

:

- That
`t = TBool`

. - That
`typecheck e = Just TBool`

.

I can get the first conclusion by

```
destruct (typecheck e) in H.
2: inversion H. (* eliminate "Nothing = Just t" case *)
destruct (t0) in H.
1: inversion H. (* eliminate "Nothing = Just t" case *)
apply unjust_preserves_equal in H.
```

where `unjust_preserves_equal`

is a simple lemma that states `forall A : Type, forall x y : A, @Just A x = @Just A y -> x = y.`

. This leaves me with the hypothesis `H : TBool = t`

, which gets me conclusion number 1 above.

This is somewhat destructive, of course, as I no longer have the structure I wanted. I presume there’s some way to “copy” `H`

so that I could avoid losing the original `match`

structure.

Setting that aside, I have *no* idea how to get conclusion number 2. `maybe`

is a simple inductive type, so I don’t see why I shouldn’t be able to reach conclusion number 2; I just have no idea how to ask Coq to extract that conclusion from the original `H`

’s `match`

expression. (I tried to write a little lemma to do this, but I couldn’t find a way to make the `TBool`

pattern a parameter to the lemma.)

Thank you!