This goal is indeed trivial in that you can return any natural number for the Empt case, and rest assured that nobody can reach that number because they first have to pass in a proper H2 : is_pos nat1 H1
.
I believe the next "correct" way to solve such a thing is to use a dependent pattern-matching, in the lines of:
Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat :=
match nat1 as nat1' return is_pos nat1' H1 -> Nat with
| Empt => fun isposEmpt =>
(* hopefully, is_pos Empt H1 immediately reduces to False, and you can do this: *)
False_rec Nat isposEmpt
| Fill Zer nat2 => fun _ => Fill One (pred nat2 H1 H2)
| Fill One nat2 => fun _ => Fill Zer nat2
end H2.
That is, you require a proof that nat1 is positive as an argument of your match, and you conclude in the Empt case that the proof is bogus, so you can return bogus too.
Hopefully this works and makes some sense. Please provide the necessary definitions next time to help people play with your example.