proposition: Lemma LS : forall p c, inv p c -> inv (fib_step p) (fib_step_cPair c).
proof: Proof. destruct p as (a,b); intros. unfold inv in *. simpl fst in *. simpl snd in *. unfold fib_step_cPair. subst; now rewrite cPairProjections1, cPairProjections2. Qed.
imports: hydras(primRec cPair extEqualNat)